def subtract_from_sum

stelliferous@0.0.2.0 · proofs/bounded_u32_arithmetic.bend:69

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

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