rw [h1]
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
⊢ (m + 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
⊢ (m * (m + 3) ^ pn + 3 * (m + 3) ^ pn) % 3 = m ^ (pn + 1) % 3