proposition: Lemma le_eq_lt_dec alpha beta: leq lt alpha beta -> {alpha = beta} + {lt alpha beta}.
proof: Proof. intro Hle. destruct (compare alpha beta) eqn:Hcomp. - apply compare_eq_iff in Hcomp as ->. now left. - apply compare_lt_iff in Hcomp. now right. - exfalso. apply compare_gt_iff in Hcomp. destruct Hle. + now apply lt_not_gt in Hcomp. + subst; now apply lt_irrefl in Hcomp. 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)