proposition: Lemma lt_not_le_flip x y : y < x → ¬x ≤ y.
proof: Proof. intros E1 E2. now destruct (le_not_lt_flip y x). Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.strong_setoids