Fieldpow.sq_four: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldpow.bend as Fieldpow
Lines 258-270 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldpow.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldpow.bend&start_line=258&end_line=270

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/field.bend as F
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend as SR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsv.bend as BV

# hv of the bits of p + 1 is 4 hv(sqrt bits)
def sq_four(+one: Nat) -> {BV.hv(L.cbits(L.bits(L.norm16([975n, 0n, 1n]))), one, 0n) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}:
  %Equal.sym(List<&2, Nat>, L.cbits(L.bits(L.norm16([975n, 0n, 1n]))), List.append(&2, Nat, F.sqrt_bits(), [0n, 0n]), sq_split()) : {BV.hv(_, one, 0n) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
  %Equal.sym(Nat, BV.hv(List.append(&2, Nat, F.sqrt_bits(), [0n, 0n]), one, 0n), BV.hv([0n, 0n], one, BV.hv(F.sqrt_bits(), one, 0n)), BV.hv_app(one, F.sqrt_bits(), 0n, [0n, 0n])) : {_ == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
  %Equal.sym(Nat, Nat.mul(0n, one), 0n, SR.zero_mul(one)) : {Nat.add(_, Nat.double(Nat.add(Nat.mul(0n, one), Nat.double(BV.hv(F.sqrt_bits(), one, 0n))))) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
  %Equal.sym(Nat, Nat.mul(0n, one), 0n, SR.zero_mul(one)) : {Nat.add(0n, Nat.double(Nat.add(_, Nat.double(BV.hv(F.sqrt_bits(), one, 0n))))) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
  %Equal.sym(Nat, Nat.double(BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), NA.double_self(BV.hv(F.sqrt_bits(), one, 0n))) : {Nat.add(0n, Nat.double(Nat.add(0n, _))) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
  %Equal.sym(Nat, Nat.add(0n, Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), SR.zero_add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))) : {Nat.add(0n, Nat.double(_)) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
  %Equal.sym(Nat, Nat.double(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))), Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))), NA.double_self(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))) : {Nat.add(0n, _) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))), NA.add_assoc(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))) : {Nat.add(0n, _) == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
  %Equal.sym(Nat, Nat.add(0n, Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))))), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))), SR.zero_add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))))) : {_ == Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))) : Nat}
  %Equal.sym(Nat, Nat.add(Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n))), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))), NA.add_assoc(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))) : {Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), Nat.add(BV.hv(F.sqrt_bits(), one, 0n), BV.hv(F.sqrt_bits(), one, 0n)))) == _ : Nat}
  {==}

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  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/crypto/secp256k1/bitsv.bend&name=hv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsv.bend&name=hv_app
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldpow.bend&name=sq_split
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend&name=zero_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend&name=zero_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=double_self
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/field.bend&name=sqrt_bits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=bits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=cbits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=norm16