proposition: Lemma not_lt_apart_lt_flip x y : ¬x < y → x ≶ y → y < x.
proof: Proof. rewrite apart_iff_total_lt. intuition. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.strong_setoids