def ud.dm_small

bend-osdev-u32@0.1.0.0 · PROOF_div.bend:119

import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

119# fewer steps than m left in the round: the remainder grows by n
120def ud.dm_small(+n: Nat, +m: Nat, +d: Nat, +r: Nat) -> {Nat.is_lt(n, 1n+m) == True{} : Bool} -> {Nat.divmod.go(n, m, d, r) == (d, Nat.add(n, r)) : Nat & Nat}:
121  match n m:
122    case 0n _:
123      h => {==}
124    case 1n+np 0n:
125      h => ud.ex_falso({Nat.divmod.go(1n+np, 0n, d, r) == (d, Nat.add(1n+np, r)) : Nat & Nat}, ud.no_lt_one(np, h))
126    case 1n+np 1n+mp:
127      h =>
128        %UL.nat_add_succ(np, r) : {Nat.divmod.go(1n+np, 1n+mp, d, r) == (d, _) : Nat & Nat}
129        ud.dm_small(np, mp, d, 1n+r, h)