proposition: Lemma Sum_cpoly_ap : forall (f : nat -> RX) a k l, (Sum k l f) ! a [=] Sum k l (fun i => (f i) ! a).
proof: Proof. unfold Sum in |- *. unfold Sum1 in |- *. intros. unfold cg_minus in |- *. astepl ((Sum0 (S l) f) ! a[+]( [--](Sum0 k f)) ! a). astepl ((Sum0 (S l) f) ! a[+][--](Sum0 k f) ! a). apply bin_op_wd_unfolded. apply Sum0_cpoly_ap. apply un_op_wd_unfolded. apply Sum0_cpoly_ap. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational