proposition: Lemma lt_succ_le_2 : forall a, nf a -> forall b, nf b -> a < succ b -> a <= b.
proof: Proof. intros c Hc; elim Hc using nf_rect. intros;apply zero_le. intros. generalize H0; case b;simpl. intros. generalize (lt_inv_nb H1). destruct 1. inversion H2. case H2;intros. inversion H4. destruct t. inversion 1. inversion H3. assert (n = n0 \/ (n < n0)%nat). omega. destruct H8. rewrite H8. case t. left. auto. right;constructor 4. auto with T1. right;constructor 3;auto. inversion H3. right;constructor 2;auto with T1. destruct b0. simpl. inversion 2. inversion H7. simpl. case b0_1;simpl. inversion 2. inversion H7. intros. inversion_clear H5. right;constructor 2;auto. right;constructor 3;auto. case (H3 b0_2 (nf_inv2 H4) H6). intro; subst b';left;auto. right;constructor 4;auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List