proposition: Lemma not_le_lt_flip `{!TrivialApart A} `{∀ x y, Decision (x = y)} x y : ¬y ≤ x → x < y.
proof: Proof. intros. destruct (le_or_lt y x); intuition. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.strong_setoids