law u32_add_nat

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

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

492law u32_add_nat:
493  for a: U32
494  for b: U32
495  for h: MNat.lt(Nat.add(U32.to_nat(a), U32.to_nat(b)), pow2(32n))
496  {U32.to_nat(U32.add(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}