proposition: Lemma projected_group : IsGroup B.
proof: Proof. split. - apply (projected_monoid f);assumption. - repeat intro; apply (injective f). rewrite op_correct, negate_correct, unit_correct, left_inverse. apply reflexivity. - repeat intro; apply (injective f). rewrite op_correct, negate_correct, unit_correct, right_inverse. reflexivity. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra