def dm_e

bend-collections-laws-crypto@1.0.0.0 · proofs/math/u64/u64div.bend:36

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend as UD

36def dm_e(+a: U32, +b: U32, +hb: {U32.is_zero(b) == False{} : Bool}) -> {Nat.add(Nat.mul(UD.v(U32.div(a, b)), UD.v(b)), UD.v(U32.mod(a, b))) == UD.v(a) : Nat}:
37  dm_e2(a, b, UD.div_mod(a, b, hb))