simp only [f0k₁, OfNat.ofNat_ne_one, ite_false, ite_eq_right_iff, neg_eq_zero]
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
⊢ f0k₁ b p ↑⟨2, ⋯⟩ = 0
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
⊢ 2 = p.pred → b = 0