proposition: Lemma bijective_applied `{Equiv A} `{Equiv B} (f : A → B) `{!Inverse f} `{!Bijective f} x: f⁻¹ (f x) = x.
proof: Proof. pose proof (setoidmor_a f). pose proof (setoidmor_b f). symmetry. now apply (bijective_cancel_left f). Qed.
imports: MathClasses.theory.setoids MathClasses.interfaces.abstract_algebra