have h1 : ((⟨2, two_lt hp5⟩ : Fin p) : ℕ) ≠ 1 := by
  intro h
  simp only [Fin.ext_iff, Fin.val_mk] at h; contradiction
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
⊢ f0k₂ a b ↑⟨2, ⋯⟩ = 0
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
h1 : ↑⟨2, ⋯⟩ ≠ 1
⊢ f0k₂ a b ↑⟨2, ⋯⟩ = 0