def double_sub
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/memory.bend:109
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend as Memory
import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
109def double_sub(+x: Nat) -> {Nat.sub(Nat.double(x), x) == x : Nat}:
110 %Equal.sym(Nat, Nat.double(x), Nat.add(x, x), NA.double_self(x)) : {Nat.sub(_, x) == x : Nat}
111 N.add_sub_cancel(x, x)