fact: Record module_on (M : abelian_group) : Type := {module_op : operation (ring_monoid R) M; module_op_lin_left_prf : op_lin_left module_op; module_op_lin_right_prf : op_lin_right module_op}.
imports: Ring_cat Operation_of_monoid