proposition: Lemma BS : forall n : Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1).
proof: Proof. intros n H1 H2 H3. unfold B in *. apply AS in H3. setoid_replace (ZnZ.of_Z (n + 1)) with (S (ZnZ.of_Z n)). - assumption. - zify. rewrite 2 ZnZ.of_Z_correct. 2-3: lia. symmetry; apply Zmod_small; lia. Qed.
imports: NZAxioms ZArith Zpow_facts DoubleType CyclicAxioms Lia