BoundedU32Arithmetic.multiply_zero_left: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend as BoundedU32Arithmetic
Lines 48-49 of stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend&start_line=48&end_line=49

import Base
import stelliferous@0.0.2.0/proofs/word_multiplication.bend as Multiplication

def multiply_zero_left(+value: U32) -> {(0 * value : U32) == 0 : U32}:
  Multiplication.native_multiply(0,value)

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mul
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_multiplication.bend&name=native_multiply