proposition: Lemma le_equiv_lt `{!TrivialApart A} `{forall x y : A, Decidable (x = y)} x y : x ≤ y -> x = y |_| x < y.
proof: Proof. intros. destruct (dec (x = y)); try auto. right. apply lt_iff_le_ne; auto. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.apartness