case zero
α : Type u_1
inst✝ : LinearOrderedSemifield α
m : ℕ
⊢ ↑(m / zero) ≤ ↑m / ↑zero

case succ
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n✝ : ℕ
⊢ ↑(m / succ n✝) ≤ ↑m / ↑(succ n✝)
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n : ℕ
⊢ ↑(m / n) ≤ ↑m / ↑n
cases n
case succ
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n✝ : ℕ
⊢ m / succ n✝ * succ n✝ ≤ m

case succ
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n✝ : ℕ
⊢ 0 < ↑(succ n✝)
case succ
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n✝ : ℕ
⊢ ↑(m / succ n✝) ≤ ↑m / ↑(succ n✝)
rw [le_div_iff, ← Nat.cast_mul, @Nat.cast_le]
case succ
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n✝ : ℕ
⊢ 0 < ↑(succ n✝)
case succ
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n✝ : ℕ
⊢ m / succ n✝ * succ n✝ ≤ m

case succ
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n✝ : ℕ
⊢ 0 < ↑(succ n✝)
exact (Nat.div_mul_le_self m _)
no goals
case zero
α : Type u_1
inst✝ : LinearOrderedSemifield α
m : ℕ
⊢ ↑(m / zero) ≤ ↑m / ↑zero
rw [cast_zero, div_zero, Nat.div_zero, cast_zero]
no goals
case succ
α : Type u_1
inst✝ : LinearOrderedSemifield α
m n✝ : ℕ
⊢ 0 < ↑(succ n✝)
exact Nat.cast_pos.2 (Nat.succ_pos _)