Theorem: Pos.succ_ne_one (Extra/Pos/Lemmas.lean)

State before:
x : Pos
⊢ x + 1 ≠ 1
Tactic:
by_toNat
State after:
x : Pos
⊢ x.toNat + 1 ≠ 1

State before:
x : Pos
⊢ x.toNat + 1 ≠ 1
Tactic:
intro h
State after:
x : Pos
h : x.toNat + 1 = 1
⊢ False

State before:
x : Pos
h : x.toNat + 1 = 1
⊢ False
Tactic:
absurd (Nat.succ.inj h)
State after:
x : Pos
h : x.toNat + 1 = 1
⊢ ¬x.toNat = 0

State before:
x : Pos
h : x.toNat + 1 = 1
⊢ ¬x.toNat = 0
Tactic:
exact Nat.ne_zero _
State after:
no goals