m n : Nat
⊢ (match m - (m + n) with
    | 0 => ofNat (m + n - m)
    | succ k => -[k+1]) =
    ↑n
m n : Nat
⊢ subNatNat (m + n) m = ↑n
unfold subNatNat
no goals
m n : Nat
⊢ (match m - (m + n) with
    | 0 => ofNat (m + n - m)
    | succ k => -[k+1]) =
    ↑n
rw [Nat.sub_eq_zero_of_le (Nat.le_add_right ..), Nat.add_sub_cancel_left, ofNat_eq_coe]