proposition: Lemma generated_ideal_included : included A generated_ideal.
proof: Proof. red in |- *. simpl in |- *. intros x H'; exists (Var R (V:=A) (Build_subtype (E:=R) (P:=A) (subtype_elt:=x) H')); split; [ idtac | try assumption ]. auto with algebra. simpl in |- *. auto with algebra. Qed.
imports: Ring_facts Generated_module