English
divMod computes the quotient and remainder of dividing a PosNum y by a PosNum d, using binary decomposition and divModAux.
Русский
divMod вычисляет частное и остаток при делении y на d для PosNum, с использованием двоичного разложения и divModAux.
LaTeX
$$def divMod (d : PosNum) : PosNum → Num × Num
| bit0 n =>
let (q, r₁) := divMod d n
divModAux d q (Num.bit0 r₁)
| bit1 n =>
let (q, r₁) := divMod d n
divModAux d q (Num.bit1 r₁)
| 1 => divModAux d 0 1$$
Lean4
/-- `divMod x y = (y / x, y % x)`. -/
def divMod (d : PosNum) : PosNum → Num × Num
| bit0 n =>
let (q, r₁) := divMod d n
divModAux d q (Num.bit0 r₁)
| bit1 n =>
let (q, r₁) := divMod d n
divModAux d q (Num.bit1 r₁)
| 1 => divModAux d 0 1
