Theorem: Int.subNatNat_le_sub (Util/Arithmetic.lean)

State before:
a b : ℕ
⊢ subNatNat a b ≤ ↑(a - b)
Tactic:
unfold subNatNat
State after:
a b : ℕ
⊢ (match b - a with
    | 0 => ofNat (a - b)
    | Nat.succ k => -[k+1]) ≤
    ↑(a - b)

State before:
a b : ℕ
⊢ (match b - a with
    | 0 => ofNat (a - b)
    | Nat.succ k => -[k+1]) ≤
    ↑(a - b)
Tactic:
split
State after:
case h_1
a b x✝ : ℕ
heq✝ : b - a = 0
⊢ ofNat (a - b) ≤ ↑(a - b)

case h_2
a b x✝ m✝ : ℕ
heq✝ : b - a = Nat.succ m✝
⊢ -[m✝+1] ≤ ↑(a - b)