law u32_divmod

bend-osdev-u32@0.1.0.0 · LAWS.bend:500

import Base

500law u32_divmod:
501  for +a: U32
502  for +b: U32
503  for h: {U32.is_zero(b) == False{} : Bool}
504  {Nat.add(Nat.mul(U32.to_nat(U32.div(a, b)), U32.to_nat(b)), U32.to_nat(U32.mod(a, b))) == U32.to_nat(a) : Nat}