Theorem: Nat.pos_of_nonzero (GMLInit/Data/Nat/IsPos.lean)

State before:
n : Nat
⊢ n ≠ 0 → n > 0
Tactic:
cases n with
| zero => intro; contradiction
| succ n => intro; exact is_pos _
State after:
no goals

State before:
case zero

⊢ 0 ≠ 0 → 0 > 0
Tactic:
intro
State after:
case zero
a✝ : 0 ≠ 0
⊢ 0 > 0

State before:
case zero
a✝ : 0 ≠ 0
⊢ 0 > 0
Tactic:
contradiction
State after:
no goals

State before:
case succ
n : Nat
⊢ n + 1 ≠ 0 → n + 1 > 0
Tactic:
intro
State after:
case succ
n : Nat
a✝ : n + 1 ≠ 0
⊢ n + 1 > 0

State before:
case succ
n : Nat
a✝ : n + 1 ≠ 0
⊢ n + 1 > 0
Tactic:
exact is_pos _
State after:
no goals