R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(match n - m with
      | 0 => ofNat (m - n)
      | succ k => -[k+1]) =
    ↑m - ↑n
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(subNatNat m n) = ↑m - ↑n
unfold subNatNat
case zero
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
e : n - m = zero
⊢ ↑(match zero with
      | 0 => ofNat (m - n)
      | succ k => -[k+1]) =
    ↑m - ↑n

case succ
R : Type u
inst✝ : AddGroupWithOne R
m n n✝ : ℕ
e : n - m = succ n✝
⊢ ↑(match succ n✝ with
      | 0 => ofNat (m - n)
      | succ k => -[k+1]) =
    ↑m - ↑n
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(match n - m with
      | 0 => ofNat (m - n)
      | succ k => -[k+1]) =
    ↑m - ↑n
cases e : n - m
case zero
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
e : n - m = zero
⊢ ↑↑(m - n) = ↑m - ↑n
case zero
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
e : n - m = zero
⊢ ↑(match zero with
      | 0 => ofNat (m - n)
      | succ k => -[k+1]) =
    ↑m - ↑n
simp only [ofNat_eq_coe]
no goals
case zero
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
e : n - m = zero
⊢ ↑↑(m - n) = ↑m - ↑n
simp [e, Nat.le_of_sub_eq_zero e]
no goals
case succ
R : Type u
inst✝ : AddGroupWithOne R
m n n✝ : ℕ
e : n - m = succ n✝
⊢ ↑(match succ n✝ with
      | 0 => ofNat (m - n)
      | succ k => -[k+1]) =
    ↑m - ↑n
rw [cast_negSucc, Nat.add_one, ← e, Nat.cast_sub <| _root_.le_of_lt <| Nat.lt_of_sub_eq_succ e,
  neg_sub]