proposition: Lemma bijective `{Equiv A} `{Equiv B} (f : A → B) `{!Inverse f} `{!Bijective f} : f⁻¹ ∘ f = id.
proof: Proof. pose proof (setoidmor_a f). apply ext_equiv_applied_iff, (bijective_applied f). Qed.
imports: MathClasses.theory.setoids MathClasses.interfaces.abstract_algebra