proposition: Lemma triangle_SumxIR : forall n (f : forall i, i < n -> IR), AbsIR (Sumx f) [<=] Sumx (fun i H => AbsIR (f i H)).
proof: Proof. simple induction n. intros; simpl in |- *. apply eq_imp_leEq; apply AbsIRz_isz. clear n; intros. simpl in |- *; eapply leEq_transitive. apply triangle_IR. apply plus_resp_leEq. eapply leEq_wdr. apply H. apply Sumx_wd. intros; algebra. Qed.
imports: CoRN.reals.OddPolyRootIR