proposition: Lemma LE_LT_eq_dec : forall alpha beta, alpha t1<= beta -> {alpha t1< beta} + {alpha = beta}.
proof: Proof. unfold LE, restrict; intros alpha beta H; decompose [and] H. apply le_eq_lt_dec in H2 as [Heq | Hlt]. - now right. - left; repeat split; auto. Defined.
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)