def add_sub

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32alg.bend:297

import Base

297def add_sub(+a: U32, +b: U32) -> {U32.sub(U32.add(a, b), a) == b : U32}:
298  match a b:
299    case U32{x} U32{y}:
300      Equal.cong(Word(32n), U32, w => U32{w}, Word.sub(32n, Word.add(32n, x, y), x), y, w_add_sub(32n, x, y))