Theorem: Nat.ball_eq_zero_iff (Logic/Vorspiel/Arith.lean)

State before:
p : ℕ → ℕ
n : ℕ
⊢ n.ball p = 0 ↔ ∃ m < n, p m = 0
Tactic:
simpa[-ball_pos_iff] using not_iff_not.mpr (ball_pos_iff (p := p) (n := n))
State after:
no goals