proposition: Lemma lt_le x y : PropHolds (x < y) -> PropHolds (x ≤ y).
proof: Proof. intro. apply lt_iff_le_apart. assumption. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.apartness