proposition: Lemma eq_iff_le x y : x = y ↔ x ≤ y ∧ y ≤ x.
proof: Proof. split; intros E. now rewrite E. now apply (antisymmetry (≤) x y). Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.strong_setoids