proposition: Lemma B_holds : forall n : Z, 0 <= n < wB -> B n.
proof: Proof. intros n [H1 H2]. apply Zbounded_induction with wB. - apply B0. - apply BS. - assumption. - assumption. Qed.
imports: NZAxioms ZArith Zpow_facts DoubleType CyclicAxioms Lia