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

State before:
n : ℕ
⊢ 0 < n.inv ↔ ¬0 < n
Tactic:
simp[inv]
State after:
no goals