proposition: Lemma le_equiv_lt `{!TrivialApart A} `{∀ x y, Decision (x = y)} x y : x ≤ y → x = y ∨ x < y.
proof: Proof. intros. destruct (decide (x = y)); try tauto. right. rewrite lt_iff_le_ne; tauto. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.strong_setoids