Modpow.pm_bit: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/natural/modpow.bend as Modpow
Lines 48-63 of bend-collections-laws-math@1.0.0.0/proofs/math/natural/modpow.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/modpow.bend&start_line=48&end_line=63

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as R

# one step: the odd bit multiplies acc by base
def pm_bit(+mp: Nat, +e2: Nat, +bit: Nat, +hbit: {Nat.is_lt(bit, 2n) == True{} : Bool}, +base: Nat, +acc: Nat) -> {Nat.mod(Nat.mul(M.pow_mod_odd(1n+mp, bit, base, acc), Nat.pow(Nat.mod(Nat.mul(base, base), 1n+mp), e2)), 1n+mp) == Nat.mod(Nat.mul(acc, Nat.pow(base, Nat.add(Nat.double(e2), bit))), 1n+mp) : Nat}:
  match bit:
    case 0n:
      %Equal.sym(Nat, Nat.add(Nat.double(e2), 0n), Nat.double(e2), A.add_zero(Nat.double(e2))) : {Nat.mod(Nat.mul(acc, Nat.pow(Nat.mod(Nat.mul(base, base), 1n+mp), e2)), 1n+mp) == Nat.mod(Nat.mul(acc, Nat.pow(base, _)), 1n+mp) : Nat}
      same_sq(mp, acc, base, e2)
    case 1n:
      +m = {1n+mp : Nat}
      +d = Nat.double(e2)
      +x = Nat.pow(Nat.mod(Nat.mul(base, base), m), e2)
      %Equal.sym(Nat, Nat.pow(base, Nat.add(d, 1n)), Nat.mul(Nat.pow(base, d), Nat.pow(base, 1n)), R.pow_add(base, d, 1n)) : {Nat.mod(Nat.mul(Nat.mod(Nat.mul(acc, base), m), x), m) == Nat.mod(Nat.mul(acc, _), m) : Nat}
      %Equal.sym(Nat, Nat.pow(base, 1n), base, A.mul_one(base)) : {Nat.mod(Nat.mul(Nat.mod(Nat.mul(acc, base), m), x), m) == Nat.mod(Nat.mul(acc, Nat.mul(Nat.pow(base, d), _)), m) : Nat}
      %Equal.sym(Nat, Nat.mul(acc, Nat.mul(Nat.pow(base, d), base)), Nat.mul(Nat.mul(acc, base), Nat.pow(base, d)), Equal.trans(Nat, Nat.mul(acc, Nat.mul(Nat.pow(base, d), base)), Nat.mul(acc, Nat.mul(base, Nat.pow(base, d))), Nat.mul(Nat.mul(acc, base), Nat.pow(base, d)), Equal.cong(Nat, Nat, z => Nat.mul(acc, z), Nat.mul(Nat.pow(base, d), base), Nat.mul(base, Nat.pow(base, d)), A.mul_comm(Nat.pow(base, d), base)), Equal.sym(Nat, Nat.mul(Nat.mul(acc, base), Nat.pow(base, d)), Nat.mul(acc, Nat.mul(base, Nat.pow(base, d))), A.mul_assoc(acc, base, Nat.pow(base, d))))) : {Nat.mod(Nat.mul(Nat.mod(Nat.mul(acc, base), m), x), m) == Nat.mod(_, m) : Nat}
      Equal.trans(Nat, Nat.mod(Nat.mul(Nat.mod(Nat.mul(acc, base), m), x), m), Nat.mod(Nat.mul(Nat.mul(acc, base), x), m), Nat.mod(Nat.mul(Nat.mul(acc, base), Nat.pow(base, d)), m), R.mod_mul_l(mp, Nat.mul(acc, base), x), same_sq(mp, Nat.mul(acc, base), base, e2))
    case 2n+z:
      Empty.absurd({Nat.mod(Nat.mul(M.pow_mod_odd(1n+mp, 2n+z, base, acc), Nat.pow(Nat.mod(Nat.mul(base, base), 1n+mp), e2)), 1n+mp) == Nat.mod(Nat.mul(acc, Nat.pow(base, Nat.add(Nat.double(e2), 2n+z))), 1n+mp) : Nat}, N.lt_zero_absurd(z, hbit))

Uses (21):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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.is_lt
  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-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_one
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_zero_absurd
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&name=mod_mul_l
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&name=pow_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/modpow.bend&name=same_sq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/natural.bend&name=pow_mod_odd