proposition: Lemma generated_ideal_minimal : forall I : ideal R, included A I -> included generated_ideal I.
proof: Proof. unfold included in |- *. simpl in |- *. intros I H' x H'0; try assumption. elim H'0; intros x0 E; elim E; intros H'1 H'2; try exact H'2; clear E H'0. generalize H'2; clear H'2; clear H'1. generalize x; clear x. elim x0. simpl in |- *. intros c x H'0; try assumption. apply H'. apply in_part_comp_l with (subtype_elt c); auto with algebra. case c; auto with algebra. intros f H'0 f0 H'1 x H'2; try assumption. simpl in H'2. apply in_part_comp_l with (sgroup_law R (FMd_lift_fun (R:=R) (V:=A) (Mod:=R:MODULE R) (inj_part A) f) (FMd_lift_fun (R:=R) (V:=A) (Mod:=R:MODULE R) (inj_part A) f0)); auto with algebra. simpl in |- *. intros x H'0; try assumption. apply in_part_comp_l with (monoid_unit R); auto with algebra. intros f H'0 x H'1; try assumption. simpl in H'1. apply in_part_comp_l with (group_inverse R (FMd_lift_fun (R:=R) (V:=A) (Mod:=R:MODULE R) (inj_part A) f)); auto with algebra. intros c f H'0 x H'1; try assumption. simpl in H'1. apply in_part_comp_l with (module_mult c (FMd_lift_fun (R:=R) (V:=A) (Mod:=R:MODULE R) (inj_part A) f)); auto with algebra. change (in_part (ring_mult c (FMd_lift_fun (R:=R) (V:=A) (Mod:=R:MODULE R) (inj_part A) f)) (subsgroup_part (submonoid_subsgroup (subgroup_submonoid (ideal_subgroup I))))) in |- *. apply ideal_prop2; auto with algebra. Qed.
imports: Ring_facts Generated_module