no goals
a : Nat
h : a ≠ 0
⊢ succ (pred a) = a
induction a with
| zero => contradiction
| succ => rfl
no goals
case zero
h : zero ≠ 0
⊢ succ (pred zero) = zero
contradiction
no goals
case succ
n✝ : Nat
n_ih✝ : n✝ ≠ 0 → succ (pred n✝) = n✝
h : succ n✝ ≠ 0
⊢ succ (pred (succ n✝)) = succ n✝
rfl