IsCRing B. Proof. split. - apply (groups.projected_ab_group f);assumption. - apply (groups.projected_com_monoid f mult_correct one_correct);assumption. - repeat intro; apply (injective f). rewrite plus_correct, !mult_correct, plus_correct. apply distribute_l. Qed.
Require Import Require Import