proposition: Lemma pow_2_n_growing : Un_growing pow_2_n.
proof: Proof. unfold Un_growing. intro. replace (S n) with (n + 1)%nat; [ unfold pow_2_n; rewrite pow_add | ring ]. pattern (2 ^ n) at 1; rewrite <- Rmult_1_r. apply Rmult_le_compat_l. - left; apply pow_lt; prove_sup0. - simpl. rewrite Rmult_1_r. pattern 1 at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; apply Rlt_0_1. Qed.
imports: Sumbool Rbase Rfunctions SeqSeries Ranalysis1 Lra