proposition: Lemma projected_ab_group: AbGroup B.
proof: Proof. split; try apply _. now apply (projected_group f). repeat intro; apply (injective f). now rewrite op_correct, commutativity. Qed.
imports: Coq.Classes.Morphisms MathClasses.interfaces.abstract_algebra