def eight

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/consts.bend:200

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

200def eight(+x: Nat) -> {Nat.mul(8n, x) == C.shift(3n, x) : Nat}:
201  %Equal.sym(Nat, Nat.add(x, 0n), x, NA.add_zero(x)) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, _))))))) == Nat.double(Nat.double(Nat.double(x))) : Nat}
202  %Equal.sym(Nat, Nat.double(x), Nat.add(x, x), NA.double_self(x)) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))))) == Nat.double(Nat.double(_)) : Nat}
203  %Equal.sym(Nat, Nat.double(Nat.add(x, x)), Nat.add(Nat.add(x, x), Nat.add(x, x)), NA.double_self(Nat.add(x, x))) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))))) == Nat.double(_) : Nat}
204  %Equal.sym(Nat, Nat.add(Nat.add(x, x), Nat.add(x, x)), Nat.add(x, Nat.add(x, Nat.add(x, x))), NA.add_assoc(x, x, Nat.add(x, x))) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))))) == Nat.double(_) : Nat}
205  %Equal.sym(Nat, Nat.double(Nat.add(x, Nat.add(x, Nat.add(x, x)))), Nat.add(Nat.add(x, Nat.add(x, Nat.add(x, x))), Nat.add(x, Nat.add(x, Nat.add(x, x)))), NA.double_self(Nat.add(x, Nat.add(x, Nat.add(x, x))))) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))))) == _ : Nat}
206  %Equal.sym(Nat, Nat.add(Nat.add(x, Nat.add(x, Nat.add(x, x))), Nat.add(x, Nat.add(x, Nat.add(x, x)))), Nat.add(x, Nat.add(Nat.add(x, Nat.add(x, x)), Nat.add(x, Nat.add(x, Nat.add(x, x))))), NA.add_assoc(x, Nat.add(x, Nat.add(x, x)), Nat.add(x, Nat.add(x, Nat.add(x, x))))) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))))) == _ : Nat}
207  %Equal.sym(Nat, Nat.add(Nat.add(x, Nat.add(x, x)), Nat.add(x, Nat.add(x, Nat.add(x, x)))), Nat.add(x, Nat.add(Nat.add(x, x), Nat.add(x, Nat.add(x, Nat.add(x, x))))), NA.add_assoc(x, Nat.add(x, x), Nat.add(x, Nat.add(x, Nat.add(x, x))))) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))))) == Nat.add(x, _) : Nat}
208  %Equal.sym(Nat, Nat.add(Nat.add(x, x), Nat.add(x, Nat.add(x, Nat.add(x, x)))), Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))), NA.add_assoc(x, x, Nat.add(x, Nat.add(x, Nat.add(x, x))))) : {Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, Nat.add(x, x))))))) == Nat.add(x, Nat.add(x, _)) : Nat}
209  {==}