BoundedU32Arithmetic.add_after_subtract: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend as BoundedU32Arithmetic
Lines 74-79 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=74&end_line=79

import Base

def add_after_subtract(+value: U32,+padding: U32,+offset: U32) ->
  {((value - padding : U32) + offset : U32) == ((value + offset : U32) - padding : U32) : U32}:
  %Equal.sym(U32,((value - padding : U32) + offset : U32),(offset + (value - padding : U32) : U32),add_commutative((value - padding : U32),offset)) :
    {_ == ((value + offset : U32) - padding : U32) : U32}
  %add_commutative(offset,value) : {(offset + (value - padding : U32) : U32) == (_ - padding : U32) : U32}
  Equal.sym(U32,((offset + value : U32) - padding : U32),(offset + (value - padding : U32) : U32),subtract_from_sum(offset,value,padding))

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend&name=add_commutative
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend&name=subtract_from_sum