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

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

State before:
x : Pos
⊢ x.toNat + 1 > 1
Tactic:
apply Nat.succ_lt_succ
State after:
case a
x : Pos
⊢ 0 < x.toNat

State before:
case a
x : Pos
⊢ 0 < x.toNat
Tactic:
exact Nat.zero_lt _
State after:
no goals