proposition: Lemma poly_inv_apply : forall (p : RX) x, (cpoly_inv _ p) ! x [=] [--]p ! x.
proof: Proof. Proof inv_apply. Lemma Sum0_cpoly_ap : forall (f : nat -> RX) a k, (Sum0 k f) ! a [=] Sum0 k (fun i => (f i) ! a). Proof. intros. induction k as [| k Hreck]. simpl in |- *. algebra. astepl (Sum0 k f[+]f k) ! a. astepl ((Sum0 k f) ! a[+](f k) ! a). astepl (Sum0 k (fun i : nat => (f i) ! a)[+](f k) ! a). simpl in |- *. algebra. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational