proposition: Lemma Bn_dist : forall n, (Bn (S n)) - Bn n <= (/ 2) ^ (S n).
proof: Proof. intros n; simpl Bn. replace (Bn n + fp (f n) n - Bn n) with (fp (f n) n) by ring. unfold fp; destruct f; simpl. apply Rle_refl. rewrite <- (Rmult_0_r 0). apply Rmult_le_compat. apply Rle_refl. apply Rle_refl. apply Rle_0_inv_2. apply pow_le; apply Rle_0_inv_2. Qed.
imports: Reals Lia Lra