def add_zero

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

import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as U32alg

import 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))

Uses (5)

Used by (4)