def ud.dm_lt

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

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

105def ud.dm_lt(+n: Nat, +m: Nat, +d: Nat, +r: Nat, +bp: Nat) -> {Nat.add(m, r) == bp : Nat} -> {Nat.is_lt(Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d, r)), 1n+bp) == True{} : Bool}:
106  match n m:
107    case 0n _:
108      h =>
109        %h : {Nat.is_lt(r, 1n+_) == True{} : Bool}
110        ud.lt_add(m, r)
111    case 1n+np 0n:
112      h => ud.dm_lt(np, r, 1n+d, 0n, bp, Equal.trans(Nat, Nat.add(r, 0n), r, bp, UL.nat_add_zero(r), h))
113    case 1n+np 1n+mp:
114      h => ud.dm_lt(np, mp, d, 1n+r, bp, Equal.trans(Nat, Nat.add(mp, 1n+r), 1n+Nat.add(mp, r), bp, UL.nat_add_succ(mp, r), h))