proposition: Lemma nth_coeff_sum0 : forall (p_ : nat -> RX) k n, nth_coeff k (Sum0 n p_) [=] Sum0 n (fun i => nth_coeff k (p_ i)).
proof: Proof. intros. induction n as [| n Hrecn]; intros. simpl in |- *. algebra. change (nth_coeff k (Sum0 n p_[+]p_ n) [=] Sum0 n (fun i : nat => nth_coeff k (p_ i)) [+]nth_coeff k (p_ n)) in |- *. Step_final (nth_coeff k (Sum0 n p_) [+]nth_coeff k (p_ n)). Qed.
imports: CoRN.algebra.CPolynomials Coq.Classes.Morphisms CoRN.algebra.CRings