proposition: Lemma Bn_growing_trans : forall n N, (Bn n) <= (Bn (N + n)).
proof: Proof. intros n N. induction N. simpl; apply Rle_refl. replace (S N + n)%nat with (S (N + n))%nat by lia. eapply Rle_trans. apply IHN. apply Bn_growing. Qed.
imports: Reals Lia Lra