proposition: Lemma alt_Build_Injective `{Equiv A} `{Equiv B} (f : A → B) `{!Inverse f} : Setoid_Morphism f → Setoid_Morphism (f⁻¹) → f⁻¹ ∘ f = id → Injective f.
proof: Proof. intros ?? E. pose proof (setoidmor_a f). pose proof (setoidmor_b f). split; try apply _. intros x y F. rewrite <-(ext_equiv_applied E x), <-(ext_equiv_applied E y). unfold compose. now rewrite F. Qed.
imports: MathClasses.theory.setoids MathClasses.interfaces.abstract_algebra