proposition: Lemma Bn_l_dist : forall n, l - Bn n <= (/2) ^ n.
proof: Proof. intros n. apply (Rplus_le_reg_l (Bn n)); ring_simplify. apply l_lub; intros m. destruct (le_ge_dec m n) as [Hd|Hd]. pattern (Bn m); rewrite <- Rplus_0_r. apply Rplus_le_compat. replace n with ((n - m) + m)%nat by lia. apply Bn_growing_trans. apply pow_le; apply Rle_0_inv_2. replace (Bn m) with (Bn n + (Bn m - Bn n)) by ring. apply Rplus_le_compat_l. replace m with ((m - n) + n)%nat by lia. eapply Rle_trans. apply Bn_dist_trans. rewrite <- Rmult_1_r. apply Rmult_le_compat_l. apply pow_le; apply Rle_0_inv_2. rewrite <- Rminus_0_r. apply Rplus_le_compat_l. apply Ropp_le_contravar. apply pow_le; apply Rle_0_inv_2. Qed.
imports: Reals Lia Lra