proposition: Lemma Le_trans alpha beta gamma : alpha o<= beta -> beta o<= gamma -> alpha o<= gamma.
proof: Proof. destruct alpha, beta, gamma; simpl. repeat rewrite Le_iff; cbn. intros; eauto with T1. eapply T1.LE_trans; eauto. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles ArithRing Wellfounded Operators_Properties Logic.Eqdep_dec) hydras(Prelude.More_Arith Prelude.Restriction Prelude.DecPreOrder ON_Generic OrdNotations)