proposition: Lemma injective_ne `{Equiv A} `{Equiv B} `(f : A → B) `{!Injective f} x y : x ≠ y → f x ≠ f y.
proof: Proof. intros E1 E2. apply E1. now apply (injective f). Qed.
imports: MathClasses.theory.setoids MathClasses.interfaces.abstract_algebra