proposition: Lemma bijective_cancel_inverse_left `{Equiv A} `{Equiv B} (f : A → B) `{!Inverse f} `{!Bijective f} x y : f⁻¹ x = y → x = f y.
proof: Proof. pose proof (setoidmor_a f). pose proof (setoidmor_b f). intros E. now rewrite <-E, (surjective_applied f). Qed.
imports: MathClasses.theory.setoids MathClasses.interfaces.abstract_algebra