def sub_double

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake3/lists.bend:92

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N

92def sub_double(+p: Nat) -> {Nat.sub(Nat.double(p),p) == p : Nat}:
93  %Equal.sym(Nat,Nat.double(p),Nat.add(p,p),double_add(p)) : {Nat.sub(_,p) == p : Nat}
94  N.add_sub_cancel(p,p)