def mod_pow

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/modpow.bend:17

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as R

17# (x mod m)^k == x^k (mod m)   (Mathlib Nat.pow_mod)
18def mod_pow(+mp: Nat, +x: Nat, +k: Nat) -> {Nat.mod(Nat.pow(Nat.mod(x, 1n+mp), k), 1n+mp) == Nat.mod(Nat.pow(x, k), 1n+mp) : Nat}:
19  match k:
20    case 0n:
21      {==}
22    case 1n+ +kp:
23      +m = {1n+mp : Nat}
24      +y = Nat.mod(x, m)
25      Equal.trans(Nat, Nat.mod(Nat.mul(y, Nat.pow(y, kp)), m), Nat.mod(Nat.mul(x, Nat.pow(y, kp)), m), Nat.mod(Nat.mul(x, Nat.pow(x, kp)), m), R.mod_mul_l(mp, x, Nat.pow(y, kp)),
26        Equal.trans(Nat, Nat.mod(Nat.mul(x, Nat.pow(y, kp)), m), Nat.mod(Nat.mul(x, Nat.mod(Nat.pow(y, kp), m)), m), Nat.mod(Nat.mul(x, Nat.pow(x, kp)), m), Equal.sym(Nat, Nat.mod(Nat.mul(x, Nat.mod(Nat.pow(y, kp), m)), m), Nat.mod(Nat.mul(x, Nat.pow(y, kp)), m), R.mod_mul_r(mp, x, Nat.pow(y, kp))),
27          Equal.trans(Nat, Nat.mod(Nat.mul(x, Nat.mod(Nat.pow(y, kp), m)), m), Nat.mod(Nat.mul(x, Nat.mod(Nat.pow(x, kp), m)), m), Nat.mod(Nat.mul(x, Nat.pow(x, kp)), m), Equal.cong(Nat, Nat, z => Nat.mod(Nat.mul(x, z), m), Nat.mod(Nat.pow(y, kp), m), Nat.mod(Nat.pow(x, kp), m), mod_pow(mp, x, kp)), R.mod_mul_r(mp, x, Nat.pow(x, kp)))))