proposition: Lemma lt_succ_le_R : forall a, nf a -> forall b, nf b -> leq lt (succ a) b -> lt a b .
proof: Proof. intros c Hc; elim Hc using nf_rect. - intros *; rewrite le_lt_eq. intros Hb [Hlt | Heq]; destruct b. + now apply not_lt_zero in Hlt. + apply zero_lt. + easy. + apply zero_lt. - intros *; rewrite le_lt_eq. intros Hb [Hlt | Heq]. + apply lt_trans with (succ (FS n)). apply lt_succ. auto. + subst. apply lt_succ. - intros * H H0 H1 H2 H3 b0 H4 ; rewrite le_lt_eq; intros [Hlt | Heq]. + apply lt_trans with (succ (cons (cons a n b) n' b')); try assumption. apply lt_succ. + subst; apply lt_succ. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)