proposition: Lemma Bn_dist_trans : forall n N, Bn (N + n) - Bn n <= (/ 2) ^ n * (1 - (/ 2) ^ N).
proof: Proof. intros n N. induction N. simpl. unfold Rminus; repeat rewrite Rplus_opp_r. rewrite Rmult_0_r. apply Rle_refl. simpl plus. replace (Bn (S (N + n)) - Bn n) with (Bn (S (N + n)) - Bn (N + n) + (Bn (N + n) - Bn n)) by ring. eapply Rle_trans. apply Rplus_le_compat. apply Bn_dist. apply IHN. repeat rewrite <- tech_pow_Rmult. rewrite pow_add. right. apply Rminus_diag_uniq; ring_simplify. replace (2 * / 2) with 1; [ring|]. symmetry; rewrite Rmult_comm; apply Rinv_l. intros Hneg. apply (Rlt_asym 1 0). rewrite <- Hneg; pattern 1 at 1; rewrite <- (Rplus_0_r 1). apply Rplus_lt_compat_l; apply Rlt_0_1. apply Rlt_0_1. Qed.
imports: Reals Lia Lra