English
Auxiliary definition for PosNum.divMod: divModAux(d, q, r) updates quotient and remainder depending on whether r ≥ d.
Русский
Вспомогательное определение для PosNum.divMod: divModAux(d, q, r) обновляет частное и остаток в зависимости от того, выполняется ли r ≥ d.
LaTeX
$$def divModAux (d : PosNum) (q r : Num) : Num × Num :=
match Num.ofZNum' (Num.sub' r (Num.pos d)) with
| some r' => (Num.bit1 q, r')
| none => (Num.bit0 q, r)$$
Lean4
/-- Auxiliary definition for `PosNum.divMod`. -/
def divModAux (d : PosNum) (q r : Num) : Num × Num :=
match Num.ofZNum' (Num.sub' r (Num.pos d)) with
| some r' => (Num.bit1 q, r')
| none => (Num.bit0 q, r)
