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

State before:
n : ℕ
⊢ n.inv = 0 ↔ 0 < n
Tactic:
simp[inv, isEqNat, zero_lt_iff]
State after:
no goals