proposition: Lemma lt_succ_le_R : forall a, nf a -> forall b, nf b -> succ a <= b -> a < b .
proof: Proof. intros c Hc; elim Hc using nf_rect. compute. intros. case H0;intros. subst b;auto with T1. eapply lt_trans. 2:eexact H1. auto with T1. intros. inversion_clear H0. subst b; simpl; auto with T1. simpl in H1. eapply lt_trans. 2:eauto. auto with T1. intros. simpl in H5. case H5. intro; subst b0. constructor 4. apply lt_succ;auto. intro. eapply lt_trans. 2:eauto. constructor 4. apply lt_succ;auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List