proposition: Lemma apart_total_lt x y : x ≶ y → x < y ∨ y < x.
proof: Proof. intros. now apply apart_iff_total_lt. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.strong_setoids