proposition: Lemma succ_mod_wB : forall n : Z, (n + 1) mod wB = ((n mod wB) + 1) mod wB.
proof: Proof. intro n. rewrite <- one_mod_wB at 2. now rewrite <- Zplus_mod. Qed.
imports: NZAxioms ZArith Zpow_facts DoubleType CyclicAxioms Lia