case zero
p' : ℕ
⊢ sZMod (p' + 2) zero = ↑(s zero)

case succ
p' i : ℕ
ih : sZMod (p' + 2) i = ↑(s i)
⊢ sZMod (p' + 2) (succ i) = ↑(s (succ i))
p' i : ℕ
⊢ sZMod (p' + 2) i = ↑(s i)
induction' i with i ih
case zero
p' : ℕ
⊢ 4 = ↑4
case zero
p' : ℕ
⊢ sZMod (p' + 2) zero = ↑(s zero)
dsimp [s, sZMod]
no goals
case zero
p' : ℕ
⊢ 4 = ↑4
norm_num
case succ
p' i : ℕ
ih : sZMod (p' + 2) i = ↑(s i)
⊢ ↑(s i) ^ 2 - 2 = ↑(s i) ^ 2 - 2
case succ
p' i : ℕ
ih : sZMod (p' + 2) i = ↑(s i)
⊢ sZMod (p' + 2) (succ i) = ↑(s (succ i))
push_cast [s, sZMod, ih]
no goals
case succ
p' i : ℕ
ih : sZMod (p' + 2) i = ↑(s i)
⊢ ↑(s i) ^ 2 - 2 = ↑(s i) ^ 2 - 2
rfl