proposition: Lemma le_or_lt `{!TrivialApart A} `{∀ x y, Decision (x = y)} x y : x ≤ y ∨ y < x.
proof: Proof. destruct (trichotomy (<) x y) as [|[|]]; try tauto. left. now apply lt_le. left. now apply eq_le_flip. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.strong_setoids