proposition: Lemma sum_growing : forall (An Bn:nat -> R) (N:nat), (forall n:nat, An n <= Bn n) -> sum_f_R0 An N <= sum_f_R0 Bn N.
proof: Proof. intros. induction N as [| N HrecN]. - simpl; apply H. - do 2 rewrite tech5. apply Rle_trans with (sum_f_R0 An N + Bn (S N)). + apply Rplus_le_compat_l; apply H. + do 2 rewrite <- (Rplus_comm (Bn (S N))). apply Rplus_le_compat_l; apply HrecN. Qed.
imports: Rbase Rfunctions Rseries Rcomplete