U32.internal_dm_take: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/u32.bend as U32
Lines 857-859 of bend-mathlib@0.8.1.0/u32.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/u32.bend&start_line=857&end_line=859

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

def internal_dm_take(+p: Nat, +q: Word(p), +b: Nat, +r2: Nat, +x: Bool, +r: Nat, -a: Nat, ea: {Nat.add(Nat.mul(Word.to_nat(p, q), b), r) == a : Nat}, hr: MNat.lt(r, b), +e2: {Nat.add(b, r2) == Nat.add(internal_bv(x), Nat.double(r)) : Nat}) -> {Nat.add(Nat.mul(1n+Nat.double(Word.to_nat(p, q)), b), r2) == Nat.add(internal_bv(x), Nat.double(a)) : Nat} & MNat.lt(r2, b):
  +ek = Equal.trans(Nat, Nat.add(Nat.mul(1n, b), r2), Nat.add(b, r2), Nat.add(internal_bv(x), Nat.double(r)), Equal.cong(Nat, Nat, z => Nat.add(z, r2), Nat.mul(1n, b), b, MNat.one_mul(b)), e2)
  (internal_div_step(1n, Word.to_nat(p, q), b, r2, internal_bv(x), r, a, ek, ea), internal_rem_lt(b, r2, Nat.add(internal_bv(x), Nat.double(r)), e2, internal_bit_double_lt(x, r, b, hr)))

Uses (17):
  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.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=Nat.mul
  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=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=lt
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=one_mul
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/u32.bend&name=internal_bit_double_lt
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/u32.bend&name=internal_bv
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/u32.bend&name=internal_div_step
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/u32.bend&name=internal_rem_lt