proposition: Lemma ideal_prop2 : forall (I : ideal) (x a : R), in_part x I -> in_part (ring_mult a x) I.
proof: Proof. intros I x a H'; try assumption. apply (ideal_prf (i:=I)); auto with algebra. Qed.
imports: Ring_facts Generated_module