no goals
m n k : Nat
⊢ subNatNat (m + n) k = ↑m + subNatNat n k
cases n.lt_or_ge k with
| inl h' =>
  simp [subNatNat_of_lt h', succ_pred_eq_of_pos (Nat.sub_pos_of_lt h')]
  conv => lhs; rw [← Nat.sub_add_cancel (Nat.le_of_lt h')]
  apply subNatNat_add_add
| inr h' => simp [subNatNat_of_le h',
    subNatNat_of_le (Nat.le_trans h' (le_add_left ..)), Nat.add_sub_assoc h']
case inl
m n k : Nat
h' : n < k
⊢ subNatNat (m + n) k = subNatNat m (k - n)
case inl
m n k : Nat
h' : n < k
⊢ subNatNat (m + n) k = ↑m + subNatNat n k
simp [subNatNat_of_lt h', succ_pred_eq_of_pos (Nat.sub_pos_of_lt h')]
case inl
m n k : Nat
h' : n < k
⊢ subNatNat (m + n) (k - n + n) = subNatNat m (k - n)
case inl
m n k : Nat
h' : n < k
⊢ subNatNat (m + n) k = subNatNat m (k - n)
conv => lhs; rw [← Nat.sub_add_cancel (Nat.le_of_lt h')]
no goals
case inl
m n k : Nat
h' : n < k
⊢ subNatNat (m + n) (k - n + n) = subNatNat m (k - n)
apply subNatNat_add_add
no goals
case inr
m n k : Nat
h' : n ≥ k
⊢ subNatNat (m + n) k = ↑m + subNatNat n k
simp [subNatNat_of_le h',
subNatNat_of_le (Nat.le_trans h' (le_add_left ..)), Nat.add_sub_assoc h']