proposition: Lemma poly_representation' : forall (f_ : nat -> RX) k, k <= n -> (Sum 0 n (fun i => f_ i[*]poly_01 i n)) ! (a_ k) [=] (f_ k) ! (a_ k).
proof: Proof. intros. apply eq_transitive_unfolded with (Sum 0 n (fun i : nat => (f_ i[*]poly_01 i n) ! (a_ k))). apply Sum_cpoly_ap with (f := fun i : nat => f_ i[*]poly_01 i n). astepl (Sum 0 n (fun i : nat => (f_ i) ! (a_ k) [*] (poly_01 i n) ! (a_ k))). astepr ((f_ k) ! (a_ k) [*][1]). astepr ((f_ k) ! (a_ k) [*] (poly_01 k n) ! (a_ k)). apply poly_representation'' with (a := fun i : nat => (f_ i) ! (a_ k) [*] (poly_01 i n) ! (a_ k)). auto. intros. Step_final ((f_ j) ! (a_ k) [*][0]). Qed.
imports: CoRN.algebra.CPoly_Degree CoRN.algebra.COrdFields2 Coq.Classes.Morphisms Coq.Sorting.Permutation