proposition: Lemma tech4 : forall (An:nat -> R) (k:R) (N:nat), 0 <= k -> (forall i:nat, An (S i) < k * An i) -> An N <= An 0%nat * k ^ N.
proof: Proof. intros; induction N as [| N HrecN]. - simpl; right; ring. - apply Rle_trans with (k * An N). + left; apply (H0 N). + replace (S N) with (N + 1)%nat; [ idtac | ring ]. rewrite pow_add; simpl; rewrite Rmult_1_r; replace (An 0%nat * (k ^ N * k)) with (k * (An 0%nat * k ^ N)); [ idtac | ring ]; apply Rmult_le_compat_l. * assumption. * apply HrecN. Qed.
imports: Rbase Rfunctions Rseries Rcomplete