proposition: Lemma monom_sum : forall (p : RX) n, degree_le n p -> p [=] Sum 0 n (fun i => monom (nth_coeff i p) i).
proof: Proof. intros. unfold RX in |- *; 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 (monom (nth_coeff i0 p) i0))). apply nth_coeff_sum with (p_ := fun i0 : nat => monom (nth_coeff i0 p) i0). elim (le_lt_dec i n); intros. apply eq_transitive_unfolded with (nth_coeff i (monom (nth_coeff i p) i)). apply Sum_term with (f := fun i0 : nat => nth_coeff i (monom (nth_coeff i0 p) i0)) (i := i). auto with arith. auto. intros. algebra. algebra. apply eq_transitive_unfolded with ([0]:R). apply Sum_zero. auto with arith. intros. cut (i0 <> i). intro. algebra. lia. algebra. Qed.
imports: CoRN.algebra.CPoly_Degree Coq(Lia)