no goals
n m : Nat
⊢ succ n - succ m = n - m
induction m with
| zero      => exact rfl
| succ m ih => apply congrArg pred ih
no goals
case zero
n : Nat
⊢ succ n - succ zero = n - zero
exact rfl
no goals
case succ
n m : Nat
ih : succ n - succ m = n - m
⊢ succ n - succ (succ m) = n - succ m
apply congrArg pred ih