proposition: Lemma lt_iff_le_ne `{!TrivialApart A} x y : x < y <-> x ≤ y /\ x <> y.
proof: Proof. transitivity (x <= y /\ apart x y). - apply lt_iff_le_apart. - split;intros [E1 E2];split;trivial;apply trivial_apart;trivial. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.apartness