proposition: Lemma le_lt_LT alpha beta : nf alpha -> nf beta -> leq lt alpha beta -> leq LT alpha beta.
proof: Proof. repeat rewrite le_lt_eq. destruct 3. left; repeat split; auto. now right. 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)