proposition: Lemma LT_trans : forall a b c:T1, a t1< b -> b t1< c -> a t1< c.
proof: Proof. unfold LT, restrict; intros a b c H H0; decompose [and] H ; decompose [and] H0; repeat split; auto. now apply lt_trans with b. 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)