U32div.rec_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 149-158 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=149&end_line=158

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD

def rec_ok(+p: Nat, +a0: Bool, +b: U32, +hi: Word(p), qr: Word(p) & U32, ih: inv(p, hi, v(b), qr), +one: Nat, +h1: {one == 1n : Nat}) -> inv(1n+p, WCon{a0, hi}, v(b), U32.divmod.go.rec(p, a0, b, qr)):
  match qr:
    case (+q, +r):
      match r:
        case U32{+rw}:
          (he, hr) = ih
          +hts = Equal.trans(Nat, Nat.add(WD.uw(32n, WD.ow(32n, Word.shl.out(32n, a0, rw))), WD.sc(32n, WD.bo(WD.ob(32n, Word.shl.out(32n, a0, rw)), one))), Nat.add(S.bit_value(a0), Nat.double(WD.uw(32n, rw))), Nat.add(S.bit_value(a0), Nat.double(v(U32{rw}))),
            WD.shl_out1(32n, one, h1, a0, rw),
            Equal.cong(Nat, Nat, z => Nat.add(S.bit_value(a0), Nat.double(z)), WD.uw(32n, rw), v(U32{rw}), Equal.sym(Nat, v(U32{rw}), WD.uw(32n, rw), vw(rw))))
          shl_ok(p, q, b, Word.shl.out(32n, a0, rw), a0, hi, v(U32{rw}), one, h1, he, hr, hts)

Uses (25):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  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.rec
  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.shl.out
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=bit_value
  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=shl_ok
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend&name=vw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=bo
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=ob
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=ow
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=shl_out1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=uw