The Coq mailing list

[julien forest <julienfore AT gmail.com>]

You can try this way. 

Require Import Arith Div2 Omega. 
Functional Scheme div2_ind := Induction for div2 Sort Prop.
Lemma div2_lt_trans : forall m n, m < n -> Div2.div2 m < n.
Proof.
intros m; functional induction (div2 m) using div2_ind.

tauto.

intros;omega.

intros.
destruct n.
omega.
apply lt_n_S.
apply IHn.
omega.
Qed.

Regards,
J.

2011/5/21 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?