proposition: Lemma poly_as_sum : forall (p : RX) n, degree_le n p -> forall x, p ! x [=] Sum 0 n (fun i => nth_coeff i p[*]x[^]i).
proof: Proof. intros. astepl (Sum 0 n (fun i : nat => _C_ (nth_coeff i p) [*]_X_[^]i)) ! x. apply eq_transitive_unfolded with (Sum 0 n (fun i : nat => (_C_ (nth_coeff i p) [*]_X_[^]i) ! x)). apply Sum_cpoly_ap with (f := fun i : nat => _C_ (nth_coeff i p) [*]_X_[^]i). apply Sum_wd. intros. astepl ((_C_ (nth_coeff i p)) ! x[*] (_X_[^]i) ! x). Step_final (nth_coeff i p[*]_X_ ! x[^]i). Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia