proposition: Lemma sum_incr : forall (An:nat -> R) (N:nat) (l:R), Un_cv (fun n:nat => sum_f_R0 An n) l -> (forall n:nat, 0 <= An n) -> sum_f_R0 An N <= l.
proof: Proof. intros; destruct (total_order_T (sum_f_R0 An N) l) as [[Hlt|Heq]|Hgt]. - left; apply Hlt. - right; apply Heq. - cut (Un_growing (fun n:nat => sum_f_R0 An n)). + intro; set (l1 := sum_f_R0 An N) in Hgt. unfold Un_cv in H; cut (0 < l1 - l). * intro; elim (H _ H2); intros. set (N0 := max x N); cut (N0 >= x)%nat. -- intro; assert (H5 := H3 N0 H4). cut (l1 <= sum_f_R0 An N0). ++ intro; unfold Rdist in H5; rewrite Rabs_right in H5. ** cut (sum_f_R0 An N0 < l1). { intro; elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H7 H6)). } apply Rplus_lt_reg_l with (- l). do 2 rewrite (Rplus_comm (- l)). apply H5. ** apply Rle_ge; apply Rplus_le_reg_l with l. rewrite Rplus_0_r; replace (l + (sum_f_R0 An N0 - l)) with (sum_f_R0 An N0); [ idtac | ring ]; apply Rle_trans with l1. { left; apply Hgt. } apply H6. ++ unfold l1; apply Rge_le; apply (growing_prop (fun k:nat => sum_f_R0 An k)). ** apply H1. ** unfold ge, N0; apply Nat.le_max_r. -- unfold ge, N0; apply Nat.le_max_l. * apply Rplus_lt_reg_l with l; rewrite Rplus_0_r; replace (l + (l1 - l)) with l1; [ apply Hgt | ring ]. + unfold Un_growing; intro; simpl; pattern (sum_f_R0 An n) at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; apply H0. Qed.
imports: Rbase Rfunctions Rseries Rcomplete