Theorem: Nat.succ_pred' (GMLInit/Data/Nat/Succ.lean)

State before:
x : Nat
h : autoParam (x > 0) _auto✝
⊢ x - 1 + 1 = x
Tactic:
cases x with
| zero => contradiction
| succ x => rfl
State after:
no goals

State before:
case zero
h : autoParam (0 > 0) _auto✝
⊢ 0 - 1 + 1 = 0
Tactic:
contradiction
State after:
no goals

State before:
case succ
x : Nat
h : autoParam (x + 1 > 0) _auto✝
⊢ x + 1 - 1 + 1 = x + 1
Tactic:
rfl
State after:
no goals