English
For a ∈ K and n ∈ ℕ, the natural floor of a divided by n equals the natural floor of a divided by n cast to Nat: ⌊a / n⌋_+ = ⌊a⌋_+ / n.
Русский
Для a ∈ K и n ∈ ℕ естественный пол на a/n равен естественному полу на a, деленному на n.
LaTeX
$$$$ \lfloor a / n \rfloor_+ = \lfloor a \rfloor_+ / n $$$$
Lean4
theorem floor_div_natCast (a : K) (n : ℕ) : ⌊a / n⌋₊ = ⌊a⌋₊ / n :=
by
rcases le_total a 0 with ha | ha
· rw [floor_of_nonpos, floor_of_nonpos ha]
· simp
apply div_nonpos_of_nonpos_of_nonneg ha n.cast_nonneg
obtain rfl | hn := n.eq_zero_or_pos
· simp
refine eq_of_forall_le_iff fun m ↦ ?_
rw [Nat.le_div_iff_mul_le hn, le_floor_iff (by positivity), le_floor_iff ha, le_div_iff₀ (by positivity), cast_mul]
