proposition: Lemma triangle_Sum2IR : forall m n (f : forall i, m <= i -> i <= n -> IR), m <= S n -> AbsIR (Sum2 f) [<=] Sum2 (fun i Hm Hn => AbsIR (f i Hm Hn)).
proof: Proof. intros. unfold Sum2 in |- *. eapply leEq_wdr. apply triangle_SumIR. assumption. apply Sum_wd'. assumption. intros. elim (le_lt_dec m i); intro; [ simpl in |- * | exfalso; apply (Nat.le_ngt m i); auto with arith ]. elim (le_lt_dec i n); intro; [ simpl in |- * | exfalso; apply (Nat.le_ngt i n); auto with arith ]. algebra. Qed.
imports: CoRN.reals.OddPolyRootIR