case inl
m : ℕ
⊢ ↑(m / 0) = ↑m / ↑0

case inr
m n : ℕ
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n
m n : ℕ
⊢ ↑(m / n) = ↑m / ↑n
rcases eq_or_ne n 0 with (rfl | hn)
no goals
case inl
m : ℕ
⊢ ↑(m / 0) = ↑m / ↑0
simp
case inr
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n
case inr
m n : ℕ
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n
have hn' := nat_cast_ne_zero.2 hn
case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑(m / n) ≤ ↑m / ↑n

case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑m / ↑n ≤ ↑(m / n)
case inr
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n
apply le_antisymm
case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ m / n * n ≤ m
case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑(m / n) ≤ ↑m / ↑n
rw [le_div hn', ← nat_cast_mul, nat_cast_le, mul_comm]
no goals
case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ m / n * n ≤ m
apply Nat.div_mul_le_self
case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ m / n < Nat.succ (m / n)
case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑m / ↑n ≤ ↑(m / n)
rw [div_le hn', ← add_one_eq_succ, ← Nat.cast_succ, ← nat_cast_mul, nat_cast_lt, mul_comm, ←
  Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero hn)]
no goals
case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ m / n < Nat.succ (m / n)
apply Nat.lt_succ_self