fact: Hypothesis oplin_r : forall (a : R) (x y : module_util_G), Equal (gen_module_op a (sgroup_law module_util_G x y)) (sgroup_law module_util_G (gen_module_op a x) (gen_module_op a y)).
imports: Module_cat Monoid_util Group_util