proposition: Lemma lt_flip x y : x < y → ¬y < x.
proof: Proof. intros E1 E2. apply (irreflexivity (<) x). now transitivity y. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.strong_setoids