proposition: Lemma morphism_ne `{Equiv A} `{Equiv B} (f : A → B) `{!Setoid_Morphism f} x y : f x ≠ f y → x ≠ y.
proof: Proof. intros E1 E2. apply E1. now apply sm_proper. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.products