English
Define split by the rule: split(0) = (0,0); split(oadd e n a) = if e = 0 then (0,n) else let (a',m) := split a in (oadd e n a', m).
Русский
Определение split по правилу: split(0) = (0,0); split(oadd e n a) = если e=0, тогда (0,n), иначе (oadd e n a', m) где (a',m)=split(a).
LaTeX
$$$\text{split}(0)=(0,0),\quad \text{split}(oadd\ e\ n\ a)=\begin{cases}(0,n), & e=0 \\ (oadd\ e\ n\ a', m), & \text{где } (a',m)=\text{split}(a).\end{cases}$$$
Lean4
/-- Calculate division and remainder of `o` mod `ω`:
`split o = (a, n)` means `o = a + n`, where `ω ∣ a`. -/
def split : ONote → ONote × ℕ
| 0 => (0, 0)
| oadd e n a =>
if e = 0 then (0, n)
else
let (a', m) := split a
(oadd e n a', m)
