proposition: Lemma ne_total_lt `{!TrivialApart A} x y : x ≠ y → x < y ∨ y < x.
proof: Proof. rewrite <-trivial_apart. now apply apart_total_lt. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.strong_setoids