def uq.u32_add

bend-osdev-algo@0.1.0.0 · proof_u32.bend:490

import Base

490# a + b <= c: U32.add(a, b) is a + b
491def uq.u32_add(a: U32, b: U32, c: U32, h: {Nat.is_le(Nat.add(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(c)) == True{} : Bool}) -> {U32.to_nat(U32.add(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}:
492  match a b c:
493    case U32{+x} U32{+y} U32{+z}:
494      uq.add_wz(32n, x, y, False{}, z, h)