English
For any natural numbers m,n, cast(m ÷ n) into α is less than or equal to m ÷ n computed in α (assuming a semifield with order).
Русский
Для любых натуральных m,n приводим m ÷ n в α и имеем не более чем m ÷ n, считая в α (при условии порядка).
LaTeX
$$$\left(\frac{m}{n} \text{ in } \mathbb{N}\right)^{\uparrow α} \le \frac{m}{n} \text{ in } α$$$
Lean4
/-- Natural division is always less than division in the field. -/
theorem cast_div_le {m n : ℕ} : ((m / n : ℕ) : α) ≤ m / n :=
by
cases n
· rw [cast_zero, div_zero, Nat.div_zero, cast_zero]
rw [le_div_iff₀, ← Nat.cast_mul, @Nat.cast_le]
· exact Nat.div_mul_le_self m _
· exact Nat.cast_pos.2 (Nat.succ_pos _)
