proposition: Lemma submodule_in_prop : forall (a : R) (x : M), in_part x N -> in_part (module_mult a x) N.
proof: Proof. intros a x H'; try assumption. apply (submodule_prop (R:=R) (M:=M) (s:=N)); auto with algebra. Qed.
imports: Sub_group Module_facts Module_util Monoid_util Group_util