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

State before:
n : ℕ
h : n ≠ 0
⊢ n.pos = 1
Tactic:
simp[pos, isLtNat, h]
State after:
no goals