proposition: Lemma lt_succ_le_2': forall a : T1, nf a -> forall b : T1, nf b -> a t1< succ b -> a t1< b \/ a = b.
proof: Proof. intros. destruct H1 as [H2 [H3 H4]]. generalize (lt_succ_le_2 H2 H0 H3); auto. intro H5. apply le_eq_lt_dec in H5 as [Heq | Hlt]; auto. left; split; auto. 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)