IsMonoid B. Proof. split. - apply (projected_sg f). assumption. - repeat intro; apply (injective f). rewrite op_correct, unit_correct, left_identity. reflexivity. - repeat intro; apply (injective f). rewrite op_correct, unit_correct, right_identity. reflexivity. Qed.
Require Import