match m, n, hyp with
| m, 0, _ => simp [minus]
| 0, _ +1, pf => contradiction
| m + 1, n + 1 , pf =>
  simp [minus]
  rw [← add_assoc]
  simp [minus_add_cancel]
m n : ℕ
hyp : n ≤ m
⊢ minus m n hyp + n = m
no goals