proposition: Lemma projected_com_sg: CommutativeSemiGroup B.
proof: Proof. split. now apply (projected_sg f). repeat intro; apply (injective f). now rewrite !op_correct, commutativity. Qed.
imports: Coq.Classes.Morphisms MathClasses.interfaces.abstract_algebra