The Coq mailing list

[frank maltman <frank.maltman AT googlemail.com>]

On Sat, 21 May 2011 21:37:55 +0200
Pierre Casteran 
<pierre.casteran AT labri.fr>
 wrote:

> Hello,
> 
>   You can easily finish you proof with a simple lemma:
> 
> Lemma div2_le : forall n, div2 n <= n.
> destruct n.
>   simpl;auto with arith.
> apply lt_le_weak. apply lt_div2. auto.
> auto with arith.
> Qed.
> 
> Then the last case  of your proof is:
> (* case S (S m) *)
> apply le_lt_trans with (S (S m)).
> apply div2_le.
> auto.
> Qed.
> 

Thanks. The 'with' form for 'apply' was certainly a major
part of what I was missing.

It would be nice to get some of these lemmas back into Coq,
actually. I'm not sure what the policy is for inclusions in
the standard libraries but they do seem generally useful. The
Div2 module seems somewhat underdeveloped (it only has one
lemma *not* concerned with parity or double).