proposition: Lemma cm_Sum_apply (l: list (cpoly_cring R)) (x: R): (cm_Sum l) ! x [=] cm_Sum (map (fun e => e ! x) l).
proof: Proof. induction l. reflexivity. change ((a [+] cm_Sum l) ! x[=]cm_Sum (map (fun e : cpoly_cring R => e ! x) (a :: l))). rewrite plus_apply, IHl. reflexivity. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational