U32.internal_div_if: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/u32.bend as U32
Lines 931-942 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=931&end_line=942

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

def internal_div_if(+md: Nat, +em: {Nat.pow(2n, 32n) == md : Nat}, +aw: Word(32n), +bw: Word(32n), z: Bool, ez: {U32.is_zero(U32{bw}) == z : Bool}) -> {U32.to_nat(U32.div.if(aw, U32{bw}, z)) == Nat.div(Word.to_nat(32n, aw), Word.to_nat(32n, bw)) : Nat}:
  match z:
    case True{}:
      +bn = Word.to_nat(32n, bw)
      +ee = Equal.trans(Bool, Nat.is_eq(bn, 0n), U32.is_zero(U32{bw}), True{}, Equal.sym(Bool, U32.is_zero(U32{bw}), Nat.is_eq(bn, 0n), u32_is_eq_to_nat(U32{bw}, 0)), ez)
      %Equal.sym(Nat, bn, 0n, MNat.eq_of_is_eq(bn, 0n, ee)) : {0n == Nat.div(Word.to_nat(32n, aw), _) : Nat}
      {==}
    case False{}:
      +bn = Word.to_nat(32n, bw)
      +ee = Equal.trans(Bool, Nat.is_eq(bn, 0n), U32.is_zero(U32{bw}), False{}, Equal.sym(Bool, U32.is_zero(U32{bw}), Nat.is_eq(bn, 0n), u32_is_eq_to_nat(U32{bw}, 0)), ez)
      +hb = MNat.pos_of_ne_zero(bn, ee)
      internal_div_fin(U32{bw}, Word.to_nat(32n, aw), hb, U32.divmod.go(32n, aw, U32{bw}), internal_dm_go(32n, aw, U32{bw}, hb, md, em))

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.pow
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.div.if
  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=U32.is_zero
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  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=eq_of_is_eq
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=pos_of_ne_zero
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/u32.bend&name=internal_div_fin
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/u32.bend&name=internal_dm_go
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/u32.bend&name=u32_is_eq_to_nat