proposition: Lemma bijective_cancel_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_b f). intros E. apply (injective f). now rewrite (surjective_applied f). Qed.
imports: MathClasses.theory.setoids MathClasses.interfaces.abstract_algebra