proposition: Lemma lt_ne x y : x < y → x ≠ y.
proof: Proof. unfold PropHolds. intros E1 E2. rewrite E2 in E1. now destruct (irreflexivity (<) y). Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.strong_setoids