The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

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.

Pierre






Quoting frank maltman 
<frank.maltman AT googlemail.com>:

> More in the same vein, unfortunately.
>
> I know intuitively that the only time div2 n < n does not
> hold is when n = 0. Unfortunately, I'm unable to work out
> how to use the fact that m < n so therefore n /= 0:
>
> Lemma div2_lt_trans : forall m n, m < n -> Div2.div2 m < n.
> Proof.
> intros m n HMN.
> induction m using Div2.ind_0_1_SS.
> (* case 0 *)
> simpl. assumption.
> (* case 1 *)
> simpl. auto with arith.
> (* case S (S m) *)
> simpl. assert (m < n) by omega. apply IHm in H.
>
> I find myself stuck here:
>
> 1 subgoal
> m : nat
> n : nat
> HMN : S (S m) < n
> IHm : m < n -> Div2.div2 m < n
> H : Div2.div2 m < n
> ______________________________________(1/1)
> S (Div2.div2 m) < n
>
> I know S (S m) < n, therefore I know m < n.
> I know div2 m < m, therefore I know ... tentatively ...
> that S (Div2.div2 m) < n...
>
> Presumably there's a better way to go about this?