def subtract_add

stelliferous@0.0.2.0 · proofs/word_subtraction.bend:78

import Base

78def subtract_add(+a: U32,+b: U32) -> {U32.sub(U32.add(a,b),b) == a : U32}:
79  match a b:
80    case U32{+x} U32{+y}:
81      %undo(32n,x,y,False{},False{}) : {U32{Word.sub(32n,Word.add(32n,x,y),y)} == U32{_} : U32}
82      {==}