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

State before:
n : ℕ
h : n ≠ 0
⊢ n.inv = 0
Tactic:
simp[inv, isEqNat, h]
State after:
no goals