proposition: Lemma Sum_degree_le : forall (f : nat -> RX) (n k l : nat), k <= S l -> (forall i, k <= i -> i <= l -> degree_le n (f i)) -> degree_le n (Sum k l f).
proof: Proof. unfold degree_le in |- *. intros. induction l as [| l Hrecl]; intros. generalize (toCle _ _ H); clear H; intro H. inversion H as [|m0 X]. unfold Sum in |- *. unfold Sum1 in |- *. simpl in |- *. apply eq_transitive with (nth_coeff m ([0]:RX)). apply nth_coeff_wd. algebra. algebra. inversion X. rename H3 into kis0. unfold Sum in |- *. unfold Sum1 in |- *. simpl in |- *. apply eq_transitive with (nth_coeff m (f 0)). apply nth_coeff_wd. cut (f 0[-][0] [=] f 0). auto. algebra. apply H0; try auto. rewrite kis0; auto. elim (le_lt_eq_dec _ _ H); intro y. apply eq_transitive_unfolded with (nth_coeff m (Sum k l f[+]f (S l))). apply nth_coeff_wd. algebra. astepl (nth_coeff m (Sum k l f) [+]nth_coeff m (f (S l))). astepr ([0][+] ([0]:R)). apply bin_op_wd_unfolded. apply Hrecl. auto with arith. intros. apply H0. auto. auto. auto. apply H0. auto with arith. auto. auto. rewrite y. unfold Sum in |- *. unfold Sum1 in |- *. simpl in |- *. apply eq_transitive_unfolded with (nth_coeff m ([0]:RX)). apply nth_coeff_wd. algebra. algebra. Qed.
imports: CoRN.algebra.CPoly_NthCoeff CoRN.algebra.CFields CoRN.tactics.Rational Lia