proposition: Lemma generated_module_minimal : forall (R : RING) (Mod : MODULE R) (A : part_set Mod) (H : submodule Mod), included A H -> included (generated_module A) H.
proof: Proof. unfold included in |- *. simpl in |- *. intros R Mod A H H' x H'0; try assumption. elim H'0; intros x0; clear H'0. generalize x; clear x. elim x0. intros c; try assumption. elim c. simpl in |- *. intros y subtype_prf x H'0; elim H'0; intros H'1 H'2; try exact H'2; clear H'0. apply in_part_comp_l with y; auto with algebra. intros f H'0 f0 H'1 x H'2; elim H'2; intros H'3 H'4; try exact H'4; clear H'2. simpl in H'4. apply in_part_comp_l with (sgroup_law Mod (FMd_lift_fun (inj_part A) f) (FMd_lift_fun (inj_part A) f0)); auto with algebra. simpl in |- *. intros x H'0; elim H'0; intros H'1 H'2; try exact H'2; clear H'0. apply in_part_comp_l with (monoid_unit Mod); auto with algebra. intros f H'0 x H'1; try assumption. elim H'1; intros H'2 H'3; simpl in H'3; clear H'1. apply in_part_comp_l with (group_inverse Mod (FMd_lift_fun (inj_part A) f)); auto with algebra. intros c f H'0 x H'1; try assumption. simpl in H'1. elim H'1; intros H'2 H'3; try exact H'3; clear H'1. apply in_part_comp_l with (module_mult c (FMd_lift_fun (inj_part A) f)); auto with algebra. Qed.
imports: Module_kernel Free_module