rw[Nat.add_mod, h2, add_zero, Nat.mod_mod, Nat.pow_succ']
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
h1 : (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn
h2 : 3 * (m + 3) ^ pn % 3 = 0
⊢ (m * (m + 3) ^ pn + 3 * (m + 3) ^ pn) % 3 = m ^ (pn + 1) % 3
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
h1 : (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn
h2 : 3 * (m + 3) ^ pn % 3 = 0
⊢ m * (m + 3) ^ pn % 3 = m * m ^ pn % 3