The Coq mailing list

[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?