English
The natural-number value of m ÷ k equals the standard quotient, with a potential minus one adjustment when m ≡ 0 (mod k).
Русский
Значение деления m на k в ℕ равно стандартному частному, с возможным уменьшением на единицу, если m делится на k.
LaTeX
$$$(m.div k) = \\begin{cases} (m \\ bmod k) \\div k - 1, & (m \\ bmod k) = 0 \\ ((m \\ bmod k) \\div k), & (m \\ bmod k)
eq 0 \\end{cases}$$$
Lean4
theorem div_coe (m k : ℕ+) : (div m k : ℕ) = ite ((m : ℕ) % (k : ℕ) = 0) ((m : ℕ) / (k : ℕ)).pred ((m : ℕ) / (k : ℕ)) :=
by
dsimp [div, modDiv]
cases (m : ℕ) % (k : ℕ) with
| zero =>
rw [if_pos rfl]
rfl
| succ n =>
rw [if_neg n.succ_ne_zero]
rfl
