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

State before:
x : Pos
⊢ ¬x + 1 ≤ 1
Tactic:
by_toNat
State after:
x : Pos
⊢ ¬1 ≥ x.toNat + 1

State before:
x : Pos
⊢ ¬1 ≥ x.toNat + 1
Tactic:
intro h
State after:
x : Pos
h : 1 ≥ x.toNat + 1
⊢ False

State before:
x : Pos
h : 1 ≥ x.toNat + 1
⊢ False
Tactic:
absurd h
State after:
x : Pos
h : 1 ≥ x.toNat + 1
⊢ ¬1 ≥ x.toNat + 1

State before:
x : Pos
h : 1 ≥ x.toNat + 1
⊢ ¬1 ≥ x.toNat + 1
Tactic:
apply Nat.not_le_of_gt
State after:
case h
x : Pos
h : 1 ≥ x.toNat + 1
⊢ x.toNat + 1 > 1

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

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