proposition: Lemma pow_2_n_infty : cv_infty pow_2_n.
proof: Proof. assert (forall N:nat, INR N <= 2 ^ N). { simple induction N. - simpl. left; apply Rlt_0_1. - intros. pattern (S n) at 2; replace (S n) with (n + 1)%nat; [ idtac | ring ]. rewrite S_INR; rewrite pow_add. simpl. rewrite Rmult_1_r. apply Rle_trans with (2 ^ n). + rewrite <- (Rplus_comm 1). rewrite <- (Rmult_1_r (INR n)). apply (poly n 1). apply Rlt_0_1. + pattern (2 ^ n) at 1; rewrite <- Rplus_0_r. rewrite <- (Rmult_comm 2). rewrite <-Rplus_diag. apply Rplus_le_compat_l. left; apply pow_lt; prove_sup0. } intros. unfold cv_infty. intro. destruct (total_order_T 0 M) as [[Hlt|<-]|Hgt]. 2:{ exists 0%nat; intros. unfold pow_2_n; apply pow_lt; prove_sup0. } 2:{ exists 0%nat; intros. apply Rlt_trans with 0. - assumption. - unfold pow_2_n; apply pow_lt; prove_sup0. } set (N := up M). assert (0 <= N)%Z. { apply le_IZR. unfold N. assert (H0 := archimed M); elim H0; intros. left; apply Rlt_trans with M; assumption. } elim (IZN N H0); intros N0 H1. exists N0. intros. apply Rlt_le_trans with (INR N0). { rewrite INR_IZR_INZ. rewrite <- H1. unfold N. assert (H3 := archimed M). elim H3; intros; assumption. } apply Rle_trans with (pow_2_n N0). { unfold pow_2_n; apply H. } apply Rge_le. apply growing_prop. 2:assumption. apply pow_2_n_growing. Qed.
imports: Sumbool Rbase Rfunctions SeqSeries Ranalysis1 Lra