proposition: Lemma projected_monoid: Monoid B.
proof: Proof. split. now apply (projected_sg f). repeat intro; apply (injective f). now rewrite op_correct, unit_correct, left_identity. repeat intro; apply (injective f). now rewrite op_correct, unit_correct, right_identity. Qed.
imports: Coq.Classes.Morphisms MathClasses.interfaces.abstract_algebra