proposition: Lemma compose_setoid_morphism `{Equiv A} `{Equiv B} `{Equiv C} (f : A → B) (g : B → C) : Setoid_Morphism f → Setoid_Morphism g → Setoid_Morphism (g ∘ f).
proof: Proof. firstorder. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.products