def internal_div_if

import bend-mathlib@0.8.1.0/u32.bend as U32

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

931def 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}:
932  match z:
933    case True{}:
934      +bn = Word.to_nat(32n, bw)
935      +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)
936      %Equal.sym(Nat, bn, 0n, MNat.eq_of_is_eq(bn, 0n, ee)) : {0n == Nat.div(Word.to_nat(32n, aw), _) : Nat}
937      {==}
938    case False{}:
939      +bn = Word.to_nat(32n, bw)
940      +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)
941      +hb = MNat.pos_of_ne_zero(bn, ee)
942      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)

Used by (1)

bend-mathlib@0.8.1.0/u32:u32_div_to_nat