proposition: Lemma poly_representation : f [=] Sum 0 n (fun i => _C_ f ! (a_ i) [*]poly_01 i n).
proof: Proof. apply identical_poly; auto. apply Sum_degree_le. auto with arith. intros. replace n with (0 + n). apply degree_le_mult. apply degree_le_c_. apply poly_01_degree. auto. auto with arith. intros. apply eq_symmetric_unfolded. astepr (_C_ f ! (a_ i)) ! (a_ i). apply poly_representation' with (f_ := fun i : nat => _C_ f ! (a_ i)). auto. Qed.
imports: CoRN.algebra.CPoly_Degree CoRN.algebra.COrdFields2 Coq.Classes.Morphisms Coq.Sorting.Permutation