English
The division operation on positive naturals behaves like the natural-number division, with the property m = (m % k) + k · (m / k).
Русский
Операция деления на ℕ⁺ ведет себя как деление в ℕ, при этом выполняется m = (m % k) + k · (m / k).
LaTeX
$$$\\forall m,k \\in \\mathbb{N}^+, \\\text{monotonic relation} \\Rightarrow m = (m \\bmod k) + k \\cdot (m \\div k)$$$
Lean4
/-- We define `m / k` in the same way as for `ℕ` except that when `m = n * k` we take
`m / k = n - 1`. This ensures that `m = (m % k) + k * (m / k)` in all cases. Later we
define a function `div_exact` which gives the usual `m / k` in the case where `k` divides `m`.
-/
def div (m k : ℕ+) : ℕ :=
(modDiv m k).2
