U64div.gdiv: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend as U64div
Lines 98-100 of bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend&start_line=98&end_line=100

import Base
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as U

def gdiv(a: U.U64, +d: U32, +c20: U32, +c12: U32, +c8: U32, +m12: U32, +m8: U32) -> U.U64:
  U.U64{+lo, +hi} = a
  g_t2(lo, hi, d, U32.add(U32.mul(U32.mod(hi, d), c12), U32.div(lo, c20)), c20, c12, c8, m12, m8)

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend&name=g_t2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64