def same_sq

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

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

39# the squared base, reduced, is x^(2 e2) under any factor c
40def same_sq(+mp: Nat, +c: Nat, +base: Nat, +e2: Nat) -> {Nat.mod(Nat.mul(c, Nat.pow(Nat.mod(Nat.mul(base, base), 1n+mp), e2)), 1n+mp) == Nat.mod(Nat.mul(c, Nat.pow(base, Nat.double(e2))), 1n+mp) : Nat}:
41  +m = {1n+mp : Nat}
42  +bb = Nat.mul(base, base)
43  +x = Nat.pow(Nat.mod(bb, m), e2)
44  %Equal.sym(Nat, Nat.pow(base, Nat.double(e2)), Nat.pow(bb, e2), pow_double(base, e2)) : {Nat.mod(Nat.mul(c, x), m) == Nat.mod(Nat.mul(c, _), m) : Nat}
45  Equal.trans(Nat, Nat.mod(Nat.mul(c, x), m), Nat.mod(Nat.mul(c, Nat.mod(x, m)), m), Nat.mod(Nat.mul(c, Nat.pow(bb, e2)), m), Equal.sym(Nat, Nat.mod(Nat.mul(c, Nat.mod(x, m)), m), Nat.mod(Nat.mul(c, x), m), R.mod_mul_r(mp, c, x)),
46    Equal.trans(Nat, Nat.mod(Nat.mul(c, Nat.mod(x, m)), m), Nat.mod(Nat.mul(c, Nat.mod(Nat.pow(bb, e2), m)), m), Nat.mod(Nat.mul(c, Nat.pow(bb, e2)), m), Equal.cong(Nat, Nat, z => Nat.mod(Nat.mul(c, z), m), Nat.mod(x, m), Nat.mod(Nat.pow(bb, e2), m), mod_pow(mp, bb, e2)), R.mod_mul_r(mp, c, Nat.pow(bb, e2))))