proposition: Lemma nth_coeff_sum : forall (p_ : nat -> RX) k m n, nth_coeff k (Sum m n p_) [=] Sum m n (fun i => nth_coeff k (p_ i)).
proof: Proof. unfold Sum in |- *. unfold Sum1 in |- *. intros. astepl (nth_coeff k (Sum0 (S n) p_) [-]nth_coeff k (Sum0 m p_)). apply cg_minus_wd; apply nth_coeff_sum0. Qed.
imports: CoRN.algebra.CPolynomials Coq.Classes.Morphisms CoRN.algebra.CRings