proposition: Lemma lt_apart_flip x y : x < y -> y ≶ x.
proof: Proof. intro. apply symmetry, lt_iff_le_apart. assumption. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.apartness