proposition: Lemma Bn_maj : forall n, Bn n <= 1.
proof: Proof. intros n. pattern (Bn n) at 1. replace (Bn n) with (Bn n - 0) by ring. replace 0 with (Bn 0) by reflexivity. replace n with (n + 0)%nat by ring. eapply Rle_trans. apply Bn_dist_trans. simpl; rewrite <- Rmult_1_r. apply Rmult_le_compat_l; [apply Rle_0_1|]. 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