proposition: Lemma lt_le x y : PropHolds (x < y) → PropHolds (x ≤ y).
proof: Proof. intro. now apply lt_iff_le_apart. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.strong_setoids