proposition: Lemma poly_as_sum'' : forall (p : RX) n, degree_le n p -> p [=] Sum 0 n (fun i => _C_ (nth_coeff i p) [*]_X_[^]i).
proof: Proof. unfold degree_le in |- *. intros. apply all_nth_coeff_eq_imp. intros. apply eq_symmetric_unfolded. apply eq_transitive_unfolded with (Sum 0 n (fun i0 : nat => nth_coeff i (_C_ (nth_coeff i0 p) [*]_X_[^]i0))). apply nth_coeff_sum with (p_ := fun i : nat => _C_ (nth_coeff i p) [*]_X_[^]i). apply eq_transitive_unfolded with (Sum 0 n (fun i0 : nat => nth_coeff i0 p[*]nth_coeff i (_X_[^]i0))). apply Sum_wd. intros. algebra. elim (le_lt_dec i n); intros. astepr (nth_coeff i p[*][1]). astepr (nth_coeff i p[*]nth_coeff i (_X_[^]i)). apply Sum_term with (i := i) (f := fun i0 : nat => nth_coeff i0 p[*]nth_coeff i (_X_[^]i0)). auto with arith. auto. intros. Step_final (nth_coeff j p[*][0]). astepr ([0]:R). apply Sum_zero. auto with arith. intros. cut (i <> i0). intro. Step_final (nth_coeff i0 p[*][0]). intro; rewrite <- H2 in H1. apply (Nat.le_ngt i n); auto. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia