m n : Nat
h : n ≤ m
k : Nat
hk : n + k = m
⊢ succ m - n = succ (m - n)
m n : Nat
h : n ≤ m
⊢ succ m - n = succ (m - n)
let ⟨k, hk⟩ := Nat.le.dest h
no goals
m n : Nat
h : n ≤ m
k : Nat
hk : n + k = m
⊢ succ m - n = succ (m - n)
rw [← hk, Nat.add_sub_cancel_left, ← add_succ, Nat.add_sub_cancel_left]