proposition: Lemma generated_module_prop_included : forall (R : RING) (Mod : MODULE R) (A : part_set Mod), included A (generated_module A).
proof: Proof. unfold included in |- *. simpl in |- *. intros R Mod A x H'; try assumption. exists (Var R (V:=A) (Build_subtype (E:=Mod) (P:=A) (subtype_elt:=x) H')); split; [ idtac | try assumption ]. auto with algebra. simpl in |- *. auto with algebra. Qed.
imports: Module_kernel Free_module