def add_zero_left

stelliferous@0.0.2.0 · proofs/bounded_u32_arithmetic.bend:45

import stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend as BoundedU32Arithmetic

import Base

45def add_zero_left(+value: U32) -> {(0 + value : U32) == value : U32}:
46  Equal.trans(U32,(0 + value : U32),(value + 0 : U32),value,add_commutative(0,value),add_zero(value))

Uses (5)

Used by (2)