proposition: Lemma ideal_prop : forall (I : ideal) (x : I) (a : R), in_part (ring_mult a (I x)) I.
proof: Proof. intros I x a; try assumption. apply (ideal_prf (i:=I)). case x; simpl in |- *; auto with algebra. Qed.
imports: Ring_facts Generated_module