fact: Record ring_on (R : abelian_group) : Type := {ring_mult_sgroup : sgroup_on R; ring_mult_monoid : monoid_on ring_mult_sgroup; ring_monoid :> monoid_on ring_mult_monoid; ring_dist_r_prf : dist_r (sgroup_law_map ring_mult_sgroup) (sgroup_law_map R); ring_dist_l_prf : dist_l (sgroup_law_map ring_mult_sgroup) (sgroup_law_map R)}.
imports: Abelian_group_cat