proposition: Lemma poly_as_sum' : forall p : RX, p [=] Sum 0 (lth_of_poly p) (fun i => _C_ (nth_coeff i p) [*]_X_[^]i).
proof: Proof. intros. apply poly_as_sum''. apply poly_degree_lth. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia