proposition: Lemma Bn_pos : forall n, 0 <= Bn n.
proof: Proof. intros n; induction n; simpl. apply Rle_refl. unfold fp; destruct f. apply Rplus_le_le_0_compat. assumption. apply pow_le; apply Rle_0_inv_2. rewrite Rplus_0_r; assumption. Qed.
imports: Reals Lia Lra