PROOFDiv.ud.dm_lt: def of bend-osdev-u32@0.1.0.0
Import: import bend-osdev-u32@0.1.0.0/PROOF_div.bend as PROOFDiv
Lines 105-114 of bend-osdev-u32@0.1.0.0/PROOF_div.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-u32@0.1.0.0/PROOF_div.bend&start_line=105&end_line=114

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

def 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}:
  match n m:
    case 0n _:
      h =>
        %h : {Nat.is_lt(r, 1n+_) == True{} : Bool}
        ud.lt_add(m, r)
    case 1n+np 0n:
      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))
    case 1n+np 1n+mp:
      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))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.divmod.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_succ
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF_div.bend&name=ud.lt_add