proposition: Lemma eq_not_lt x y : x = y → ¬x < y.
proof: Proof. intros E. rewrite E. now apply (irreflexivity (<)). Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.strong_setoids