def cancel

bend-collections-laws-math@1.0.0.0 · proofs/math/random/chacha8/rounds.bend:30

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A

30# x + c - c = x
31def cancel(+x: U32, +c: U32) -> {U32.sub(U32.add(x,c),c) == x : U32}:
32  %A.comm(c,x) : {U32.sub(_,c) == x : U32}
33  A.add_sub(c,x)