proposition: Lemma LE_antisym (alpha beta : T1): alpha t1<= beta -> beta t1<= alpha -> alpha = beta.
proof: Proof. unfold LE; intros [Hnf_alpha [Hle_alpha_beta Hnf_beta]] [Hnf_beta2 [Hle_beta_alpha Hnf_alpha2]]. generalize (compare_reflectR alpha beta). destruct (lt_eq_lt_dec alpha beta) as [[Hlt | Heq] | Hgt]; intro H; symmetry in H. - now apply compare_lt_iff, lt_not_ge in H. - now apply compare_eq_iff in H. - now apply compare_gt_iff, lt_not_ge in H. 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)