proposition: Lemma cr_Product_apply (l: list (cpoly_cring R)) (x: R): (cr_Product l) ! x [=] cr_Product (map (fun e => e ! x) l).
proof: Proof. induction l. simpl. rewrite cring_mult_zero. apply cm_rht_unit_unfolded. change ((a [*] cr_Product l) ! x[=]cr_Product (map (fun e : cpoly_cring R => e ! x) (a :: l))). rewrite mult_apply, IHl. reflexivity. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational