proposition: Lemma surjective_proper `{Equiv A} `{Equiv B} (f g : A → B) `{!Inverse f} `{!Inverse g} `{!Surjective g} : f = g → f⁻¹ = g⁻¹ → Surjective f.
proof: Proof. intros E1 E2. pose proof (setoidmor_a g). pose proof (setoidmor_b g). split. intros ? ? E3. change (f (f⁻¹ x) = y). rewrite <-E3, (ext_equiv_applied E1 _), (ext_equiv_applied E2 _). now apply surjective_applied. rewrite E1; apply _. Qed.
imports: MathClasses.theory.setoids MathClasses.interfaces.abstract_algebra