have h2 : ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) ≠ 2 :=
  by
  intro h
  simp only [Fin.ext_iff, Fin.val_mk] at h; contradiction
p : ℕ
hpri : p.Prime
a : ℤ
⊢ f1k₂ a ↑⟨1, ⋯⟩ = 0
p : ℕ
hpri : p.Prime
a : ℤ
h2 : ↑⟨1, ⋯⟩ ≠ 2
⊢ f1k₂ a ↑⟨1, ⋯⟩ = 0