The Coq mailing list

[dehlinge AT dpt-info.u-strasbg.fr]

If you tried to run the proof script of the well-foundedness of l that I
provided, you didn't fail to notice there was a slight problem with it.
Here is the corrected version:

Lemma WFL :
        well_founded l.
Proof.
intro n.
apply (lt_wf_ind n (Acc l)).
clear n.
intros n rec.
constructor.
intros y l1.
inversion l1.
generalize l1.
rewrite <- H0.
rewrite H1.
clear H1 H0 n0 l1 y.
intros.
constructor.
intros.
inversion H0.
 elim (not_even_and_odd (S n)); auto with arith.
  apply rec.
    destruct n.
   elim H1.
     auto.
   unfold lt in |- *.
     rewrite minus_Sn_m.
    simpl in |- *.
      rewrite <- minus_n_O.
      apply le_S.
      apply le_n.
    do 2 apply le_n_S.
      destruct n.
     inversion H.
       inversion H6.
     apply le_n_S.
       apply le_O_n.
 apply rec.
   destruct n.
inversion H0.
  unfold lt in |- *.
    apply le_n_S.
    simpl in |- *.
    apply le_minus.
Defined.