induction' n with pn hpn
m n : ℕ
⊢ (m + 3) ^ n % 3 = m ^ n % 3
case zero
m : ℕ
⊢ (m + 3) ^ 0 % 3 = m ^ 0 % 3

case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
⊢ (m + 3) ^ (pn + 1) % 3 = m ^ (pn + 1) % 3