proposition: Lemma triangle_SumIR : forall k l s, k <= S l -> AbsIR (Sum k l s) [<=] Sum k l (fun i => AbsIR (s i)).
proof: Proof. intros. induction l as [| l Hrecl]. generalize (toCle _ _ H); clear H; intro H. inversion H as [|m H0 H1]. unfold Sum in |- *. unfold Sum1 in |- *. simpl in |- *. rstepr ZeroR. astepr (AbsIR [0]). apply eq_imp_leEq. apply AbsIR_wd. rational. inversion H0. unfold Sum in |- *. unfold Sum1 in |- *. simpl in |- *. rstepr (ABSIR (s 0)). apply eq_imp_leEq. apply AbsIR_wd. rational. elim (le_lt_eq_dec k (S (S l))); try intro y. apply leEq_wdl with (AbsIR (Sum k l s[+]s (S l))). apply leEq_wdr with (Sum k l (fun i : nat => AbsIR (s i)) [+]AbsIR (s (S l))). apply leEq_transitive with (AbsIR (Sum k l s) [+]AbsIR (s (S l))). apply triangle_IR. apply plus_resp_leEq. apply Hrecl. auto with arith. apply eq_symmetric_unfolded. apply Sum_last with (f := fun i : nat => AbsIR (s i)). apply AbsIR_wd. apply eq_symmetric_unfolded. apply Sum_last. rewrite y. unfold Sum in |- *. unfold Sum1 in |- *. simpl in |- *. rstepr ZeroR. astepr (AbsIR [0]). apply eq_imp_leEq. apply AbsIR_wd. rational. auto. Qed.
imports: CoRN.reals.OddPolyRootIR