have hpred : ((⟨2, two_lt hp5⟩ : Fin p) : ℕ) ≠ p.pred := by
  intro h
  simp only [Fin.ext_iff, Fin.val_mk] at h
  replace h := h.symm
  rw [Nat.pred_eq_sub_one] at h
  omega
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
⊢ f0k₁ b p ↑⟨2, ⋯⟩ = 0
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
⊢ f0k₁ b p ↑⟨2, ⋯⟩ = 0