English
Define a function modDivAux(k, r, q) for k ∈ ℕ_{>0}, r ∈ ℕ, q ∈ ℕ, returning a pair (m, t) with m ∈ ℕ_{>0} and t ∈ ℕ, by the rules: if r = 0 then m = k and t = q − 1; if r > 0 (i.e., r = r' + 1) then m = r' + 1 and t = q. This encodes a division with remainder convention similar to ℕ, with a specific adjustment when the remainder would be zero.
Русский
Определим функцию modDivAux(k, r, q) для k ∈ ℕ_{>0}, r ∈ ℕ, q ∈ ℕ, возвращающую пару (m, t) с m ∈ ℕ_{>0} и t ∈ ℕ так: если r = 0, то m = k и t = q − 1; если r > 0 (то есть r = r' + 1), то m = r' + 1 и t = q. Это задаёт разложение m = (m mod k) + k·(m / k) с заданной договорённостью.
LaTeX
$$$\\operatorname{modDivAux}(k,r,q) = \\begin{cases} (k, q-1), & r=0, \\\\ (r+1, q), & r>0. \\end{cases}$$$
Lean4
/-- We define `m % k` and `m / k` in the same way as for `ℕ`
except that when `m = n * k` we take `m % k = k` and
`m / k = n - 1`. This ensures that `m % k` is always positive
and `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 modDivAux : ℕ+ → ℕ → ℕ → ℕ+ × ℕ
| k, 0, q => ⟨k, q.pred⟩
| _, r + 1, q => ⟨⟨r + 1, Nat.succ_pos r⟩, q⟩
