proposition: Lemma LT_succ_LE_2: forall alpha beta : T1, nf beta -> alpha t1< succ beta -> alpha t1<= beta.
proof: Proof. intros. split; eauto with T1. split; eauto with T1. apply lt_succ_le_2; eauto with T1. 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)