fact: Record submodule : Type := {submodule_subgroup : subgroup M; submodule_prop : forall (a : R) (x : M), in_part x submodule_subgroup -> in_part (module_mult a x) submodule_subgroup}.
imports: Sub_group Module_facts Module_util Monoid_util Group_util