Modexp.sq_step: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/modexp.bend as Modexp
Lines 9-16 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/modexp.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/modexp.bend&start_line=9&end_line=16

import Base
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/math/natural/arith.bend as NR

def sq_step(+mp: Nat, +x: Nat, +e: Nat, +a: Nat, +he: {a == Nat.mod(Nat.pow(x, e), 1n+mp) : Nat}) -> {Nat.mod(Nat.mul(a, a), 1n+mp) == Nat.mod(Nat.pow(x, Nat.double(e)), 1n+mp) : Nat}:
  %Equal.sym(Nat, a, Nat.mod(Nat.pow(x, e), 1n+mp), he) : {Nat.mod(Nat.mul(_, a), 1n+mp) == Nat.mod(Nat.pow(x, Nat.double(e)), 1n+mp) : Nat}
  %Equal.sym(Nat, a, Nat.mod(Nat.pow(x, e), 1n+mp), he) : {Nat.mod(Nat.mul(Nat.mod(Nat.pow(x, e), 1n+mp), _), 1n+mp) == Nat.mod(Nat.pow(x, Nat.double(e)), 1n+mp) : Nat}
  %Equal.sym(Nat, Nat.mod(Nat.mul(Nat.mod(Nat.pow(x, e), 1n+mp), Nat.mod(Nat.pow(x, e), 1n+mp)), 1n+mp), Nat.mod(Nat.mul(Nat.pow(x, e), Nat.mod(Nat.pow(x, e), 1n+mp)), 1n+mp), NR.mod_mul_l(mp, Nat.pow(x, e), Nat.mod(Nat.pow(x, e), 1n+mp))) : {_ == Nat.mod(Nat.pow(x, Nat.double(e)), 1n+mp) : Nat}
  %Equal.sym(Nat, Nat.mod(Nat.mul(Nat.pow(x, e), Nat.mod(Nat.pow(x, e), 1n+mp)), 1n+mp), Nat.mod(Nat.mul(Nat.pow(x, e), Nat.pow(x, e)), 1n+mp), NR.mod_mul_r(mp, Nat.pow(x, e), Nat.pow(x, e))) : {_ == Nat.mod(Nat.pow(x, Nat.double(e)), 1n+mp) : Nat}
  %Equal.sym(Nat, Nat.double(e), Nat.add(e, e), NA.double_self(e)) : {Nat.mod(Nat.mul(Nat.pow(x, e), Nat.pow(x, e)), 1n+mp) == Nat.mod(Nat.pow(x, _), 1n+mp) : Nat}
  %Equal.sym(Nat, Nat.pow(x, Nat.add(e, e)), Nat.mul(Nat.pow(x, e), Nat.pow(x, e)), NR.pow_add(x, e, e)) : {Nat.mod(Nat.mul(Nat.pow(x, e), Nat.pow(x, e)), 1n+mp) == Nat.mod(_, 1n+mp) : Nat}
  {==}

Uses (11):
  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.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.pow
  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/proofs/math/natural/arith.bend&name=mod_mul_l
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=mod_mul_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=pow_add