have h0 : 0 < p := by linarith
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0