proposition: Theorem compare_reflectR ( alpha beta : T1) : (match lt_eq_lt_dec alpha beta with | inleft (left _) => Lt | inleft (right _) => Eq | inright _ => Gt end) = compare alpha beta.
proof: Proof. destruct (lt_eq_lt_dec alpha beta) as [[Hlt | Heq]| Hgt]; symmetry. + now apply compare_lt_iff. + now apply compare_eq_iff. + now apply compare_gt_iff. 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)