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