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

State before:
n : ℕ
h : n = 1
⊢ 0 < n
Tactic:
simp[h]
State after:
no goals