proposition: Lemma injective_compose_cancel `{Equiv A} `{Equiv B} `{Equiv C} (f : B → C) `{!Injective f} `{!Setoid_Morphism (g : A → B)} `{!Setoid_Morphism (h : A → B)} : f ∘ g = f ∘ h → g = h.
proof: Proof. pose proof (setoidmor_a g). intros E. apply setoids.ext_equiv_applied_iff. intros x. apply (injective f). now apply E. Qed.
imports: MathClasses.theory.setoids MathClasses.interfaces.abstract_algebra