IsGroup B. 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.
Require Import