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

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