def add_zero
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as U32algimport Base
294def add_zero(+b: U32) -> {U32.add(b, 0) == b : U32}:
295 Equal.trans(U32, U32.add(b, 0), U32.add(0, b), b, U32.add_comm(b, 0), zero_add(b))
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as U32algimport Base
294def add_zero(+b: U32) -> {U32.add(b, 0) == b : U32}:
295 Equal.trans(U32, U32.add(b, 0), U32.add(0, b), b, U32.add_comm(b, 0), zero_add(b))