proposition: Lemma tech6 : forall (An:nat -> R) (k:R) (N:nat), 0 <= k -> (forall i:nat, An (S i) < k * An i) -> sum_f_R0 An N <= An 0%nat * sum_f_R0 (fun i:nat => k ^ i) N.
proof: Proof. intros; induction N as [| N HrecN]. - simpl; right; ring. - apply Rle_trans with (An 0%nat * sum_f_R0 (fun i:nat => k ^ i) N + An (S N)). + rewrite tech5; do 2 rewrite <- (Rplus_comm (An (S N))); apply Rplus_le_compat_l. apply HrecN. + rewrite tech5; rewrite Rmult_plus_distr_l; apply Rplus_le_compat_l. apply tech4; assumption. Qed.
imports: Rbase Rfunctions Rseries Rcomplete