Consts.eight: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend as Consts
Lines 200-209 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend&start_line=200&end_line=209

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

def eight(+x: Nat) -> {Nat.mul(8n, x) == C.shift(3n, x) : Nat}:
  %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}
  %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}
  %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}
  %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}
  %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}
  %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}
  %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}
  %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}
  {==}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=double_self
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift