proposition: Lemma projected_ring: IsRing B.
proof: 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.
imports: HoTT.Classes.theory.groups HoTT.Classes.theory.apartness HoTT.Classes.interfaces.abstract_algebra