case pos
m n : ℕ
h : m ≥ n
⊢ ↑m - ↑n ≤ ↑(m - n)

case neg
m n : ℕ
h : ¬m ≥ n
⊢ ↑m - ↑n ≤ ↑(m - n)
m n : ℕ
⊢ ↑m - ↑n ≤ ↑(m - n)
by_cases h : m ≥ n
no goals
case pos
m n : ℕ
h : m ≥ n
⊢ ↑m - ↑n ≤ ↑(m - n)
exact le_of_eq (Int.ofNat_sub h).symm
no goals
case neg
m n : ℕ
h : ¬m ≥ n
⊢ ↑m - ↑n ≤ ↑(m - n)
simp [le_of_not_ge h, ofNat_le]