law u32_add_mod

bend-kit-lemmas@0.1.1.0 · lemmas.bend:504

import Base

504law u32_add_mod:
505  for a: U32
506  for b: U32
507  {U32.to_nat(U32.add(a, b)) == Nat.mod(Nat.add(U32.to_nat(a), U32.to_nat(b)), pow2(32n)) : Nat}