proposition: Lemma projected_group: Group B.
proof: Proof. split; try apply _. now apply (projected_monoid f). repeat intro; apply (injective f). now rewrite op_correct, negate_correct, unit_correct, left_inverse. repeat intro; apply (injective f). now rewrite op_correct, negate_correct, unit_correct, right_inverse. Qed.
imports: Coq.Classes.Morphisms MathClasses.interfaces.abstract_algebra