case inl
m n : ℕ
h : m ≤ n
⊢ ↑(m - n) = ↑m - ↑n

case inr
m n : ℕ
h : n ≤ m
⊢ ↑(m - n) = ↑m - ↑n
m n : ℕ
⊢ ↑(m - n) = ↑m - ↑n
cases' le_total m n with h h
case inl
m n : ℕ
h : m ≤ n
⊢ ↑0 = 0
case inl
m n : ℕ
h : m ≤ n
⊢ ↑(m - n) = ↑m - ↑n
rw [tsub_eq_zero_iff_le.2 h, Ordinal.sub_eq_zero_iff_le.2 (nat_cast_le.2 h)]
no goals
case inl
m n : ℕ
h : m ≤ n
⊢ ↑0 = 0
rfl
case inr
m n : ℕ
h : n ≤ m
⊢ ↑n + ↑(m - n) = ↑n + (↑m - ↑n)
case inr
m n : ℕ
h : n ≤ m
⊢ ↑(m - n) = ↑m - ↑n
apply (add_left_cancel n).1
no goals
case inr
m n : ℕ
h : n ≤ m
⊢ ↑n + ↑(m - n) = ↑n + (↑m - ↑n)
rw [← Nat.cast_add, add_tsub_cancel_of_le h, Ordinal.add_sub_cancel_of_le (nat_cast_le.2 h)]