proposition: Theorem LE_trans (alpha beta gamma: T1): alpha t1<= beta -> beta t1<= gamma -> alpha t1<= gamma.
proof: Proof. unfold LE, restrict; intros H H0; decompose [and] H ; decompose [and] H0; repeat split; auto. now apply le_trans with beta. 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)