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

import Base
import stelliferous@0.0.2.0/proofs/word_subtraction.bend as Subtraction

def subtract_from_sum(+a: U32,+b: U32,+c: U32) -> {((a + b : U32) - c : U32) == (a + (b - c : U32) : U32) : U32}:
  %Subtraction.add_subtract(b,c) : {((a + _ : U32) - c : U32) == (a + (b - c : U32) : U32) : U32}
  %add_associative(a,(b - c : U32),c) : {(_ - c : U32) == (a + (b - c : U32) : U32) : U32}
  Subtraction.subtract_add((a + (b - c : U32) : U32),c)

Uses (6):
  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_associative
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_subtraction.bend&name=add_subtract
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_subtraction.bend&name=subtract_add