proposition: Theorem add_succ_l : forall n m, (S n) + m == S (n + m).
proof: Proof. intros n m. zify. rewrite succ_mod_wB. repeat rewrite Zplus_mod_idemp_l; try apply gt_wB_0. rewrite <- (Z.add_assoc ([| n |] mod wB) 1 [| m |]). rewrite Zplus_mod_idemp_l. rewrite (Z.add_comm 1 [| m |]); now rewrite Z.add_assoc. Qed.
imports: NZAxioms ZArith Zpow_facts DoubleType CyclicAxioms Lia