proposition: Lemma lt_succ_le : forall a, nf a -> forall b, nf b -> a < b -> succ a <= b.
proof: Proof. induction a. intros H0 c'; case c'. inversion 2. destruct t. destruct n. intros. inversion_clear H. simpl. left;auto. inversion H2. simpl;case n. right;constructor 3;auto with arith. right; constructor 3;auto with arith. simpl;right;constructor 2; auto with T1. inversion 3. simpl;constructor 2;auto with T1. generalize H6;case a1. constructor 2;auto with T1. constructor 2. auto. simpl. case a1. assert (S n = n' \/ (S n < n')%nat). omega. case H7. intro; subst n'. case b'. left;auto. right;constructor 4;auto with T1. right;constructor 3;auto. intros. right;constructor 3;auto. subst b;generalize H0;case a1. intro. assert (b'=zero). inversion_clear H3. auto. inversion H7. subst b'; inversion H6. simpl. intros. case (IHa2 (nf_inv2 H) b'). eapply nf_inv2;eauto. auto. destruct 1;left;auto. intro;apply le_tail. right;auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List