proposition: Lemma le_not_lt_flip x y : y ≤ x → ¬x < y.
proof: Proof. rewrite lt_iff_le_apart. intros E1 [E2a E2b]. contradict E2b. setoid_replace x with y. now apply (irreflexivity _). now apply (antisymmetry (≤)). Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.strong_setoids