x % b ^ (k + 1)

Stream: Is there code for X?

[Kim Morrison]

Do we have

theorem Nat.mod_pow_succ {x b k : Nat} : x % b ^ (k + 1) = x % b ^ k + b ^ k * ((x / b ^ k) % b) := sorry

somewhere?

(Preference if possible for a low- or no-import proof. I don't mind at all specializing to b = 2.)

[Arend Mellendijk]

How about this:

import Mathlib.Data.Nat.Order.Basic
import Mathlib.Data.Nat.ModEq

example {a b x : Nat} : x % (a*b) = x % a + a * (x / a % b) := by
  rw [add_comm, ← Nat.div_add_mod (x % (a*b)) a, Nat.mod_mul_right_mod,
    Nat.mod_mul_right_div_self]

[Kim Morrison]

Thanks @Arend Mellendijk, I extracted a no-imports version from that.