def sub_add

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32alg.bend:302

import Base

302def sub_add(+v: U32, +a: U32) -> {U32.add(U32.sub(v, a), a) == v : U32}:
303  match v a:
304    case U32{x} U32{y}:
305      Equal.cong(Word(32n), U32, w => U32{w}, Word.add(32n, Word.sub(32n, x, y), y), x, w_sub_add(32n, x, y))