U32div.go_ok: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as U32div
Lines 160-166 of bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend&start_line=160&end_line=166

import Base

# the invariant holds for every prefix of the dividend
def go_ok(+m: Nat, +a: Word(m), +b: U32, +hb: {Nat.is_lt(0n, v(b)) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}) -> inv(m, a, v(b), U32.divmod.go(m, a, b)):
  match m a:
    case 0n WNil{}:
      ({==}, hb)
    case 1n+p WCon{a0, hi}:
      rec_ok(p, a0, b, hi, U32.divmod.go(p, hi, b), go_ok(p, hi, b, hb, one, h1), one, h1)

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.divmod.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend&name=inv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend&name=rec_ok
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend&name=v