proposition: Lemma lt_iff_le_ne `{!TrivialApart A} x y : x < y ↔ x ≤ y ∧ x ≠ y.
proof: Proof. rewrite <-trivial_apart. now apply lt_iff_le_apart. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.strong_setoids