proposition: Lemma pred_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 Zminus_mod. Qed.
imports: NZAxioms ZArith Zpow_facts DoubleType CyclicAxioms Lia