import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/w64.bend as SW
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../../src/math/natural.bend as M
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/word.bend as WD
import ../../lib/u32div.bend as UD
import ../../lib/lemmas/spec/numeric.bend as S
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/arith.bend as NR
import ../natural/sqrtn.bend as SQ2
import ../u64/u64.bend as P64
import ./width.bend as WW
import ./u32laws.bend as LW
import ./w64add.bend as WA
import ./w64mul.bend as W64M
import ./w64sqrt.bend as W64S
import ./w64sh.bend as SH
import ./w64m128.bend as M128
import ./w64div.bend as W64D
import ./w64dm.bend as DM
import ./natlight.bend as AQ
import ./montnat.bend as MN
import ./u64mont.bend as UM

# src/math/w64.bend's 32-bit Montgomery multiplication (R = 2^32) for the
# U32 pow_mod: redc32(t) for t < m^2 is t / 2^32 mod m, so
# mont32(a, b) 2^32 == a b (mod m) with mont32(a, b) < m; the loop runs the
# generic binary exponentiation on the forms x 2^32 mod m.

def v(+x: U32) -> Nat:
  U32.to_nat(x)

def true_ne_false(+h: {True{} == False{} : Bool}) -> Empty:
  LW.true_ne_false(h)

def b32v(c: Bool) -> {v(X.b32(c)) == S.bit_value(c) : Nat}:
  match c:
    case True{}:
      {==}
    case False{}:
      {==}

# x + y == (x + y mod 2^32) + 2^32 carry
def cadd(+x: U32, +y: U32) -> {Nat.add(v(x), v(y)) == Nat.add(v(U32.add(x, y)), C.shift(32n, S.bit_value(U32.is_lt(U32.add(x, y), x)))) : Nat}:
  +e1 = Equal.cong(Bool, Nat, z => Nat.add(v(U32.add(x, y)), C.shift(32n, S.bit_value(z))), U32.is_lt(U32.add(x, y), x), P64.carry32(x, y), P64.add_lt(x, y))
  Equal.trans(Nat, Nat.add(v(x), v(y)), Nat.add(v(U32.add(x, y)), C.shift(32n, S.bit_value(P64.carry32(x, y)))), Nat.add(v(U32.add(x, y)), C.shift(32n, S.bit_value(U32.is_lt(U32.add(x, y), x)))), Equal.sym(Nat, Nat.add(v(U32.add(x, y)), C.shift(32n, S.bit_value(P64.carry32(x, y)))), Nat.add(v(x), v(y)), WA.acons(x, y)), Equal.sym(Nat, Nat.add(v(U32.add(x, y)), C.shift(32n, S.bit_value(U32.is_lt(U32.add(x, y), x)))), Nat.add(v(U32.add(x, y)), C.shift(32n, S.bit_value(P64.carry32(x, y)))), e1))

# the two words of a 32 x 32 product
def m32v(+a: U32, +b: U32) -> {Nat.add(v(X.lo(X.mul32(a, b))), C.shift(32n, v(X.hi(X.mul32(a, b))))) == Nat.mul(v(a), v(b)) : Nat}:
  Equal.trans(Nat, Nat.add(v(X.lo(X.mul32(a, b))), C.shift(32n, v(X.hi(X.mul32(a, b))))), SW.value(X.mul32(a, b)), Nat.mul(v(a), v(b)), Equal.sym(Nat, SW.value(X.mul32(a, b)), Nat.add(v(X.lo(X.mul32(a, b))), C.shift(32n, v(X.hi(X.mul32(a, b))))), WA.val_eta(X.mul32(a, b))), W64M.mul32_value(a, b))

def kv(c1: Bool, c2: Bool) -> {v(U32.add(X.b32(c1), X.b32(c2))) == Nat.add(S.bit_value(c1), S.bit_value(c2)) : Nat}:
  match c1 c2:
    case True{} True{}:
      {==}
    case True{} False{}:
      {==}
    case False{} True{}:
      {==}
    case False{} False{}:
      {==}

def lo32(+w: WU.U64, +h: {C.fits(32n, SW.value(w)) == True{} : Bool}) -> {v(X.lo(w)) == SW.value(w) : Nat}:
  match w:
    case WU.U64{+l, +hh}:
      Equal.trans(Nat, v(l), C.low(32n, SW.value(WU.U64{l, hh})), SW.value(WU.U64{l, hh}), Equal.sym(Nat, C.low(32n, Nat.add(v(l), C.shift(32n, v(hh)))), v(l), WW.low_u(32n, v(l), v(hh), LW.vb(l))), WW.low_fit(32n, SW.value(WU.U64{l, hh}), h))


# sub_if32: r < 2 m gives r mod m
def sif_c(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +r: WU.U64, +hM: {v(m) == 1n+bp : Nat}, +hr: {Nat.is_lt(SW.value(r), Nat.add(1n+bp, 1n+bp)) == True{} : Bool}, +c: Bool, +hc: {X.le(WU.U64{m, 0}, r) == c : Bool}) -> {v(X.sub_if32(r, m, c)) == Nat.mod(SW.value(r), 1n+bp) : Nat}:
  match c:
    case True{}:
      +hmv = Equal.trans(Nat, SW.value(WU.U64{m, 0}), v(m), 1n+bp, M128.val0(m), hM)
      +hm32 = WW.lt_one(32n, one, h1, 1n+bp, L.subst(Nat, z => {C.fits(32n, z) == True{} : Bool}, v(m), 1n+bp, hM, LW.vb(m)))
      +hle0 = Equal.trans(Bool, Nat.is_le(SW.value(WU.U64{m, 0}), SW.value(r)), X.le(WU.U64{m, 0}, r), True{}, Equal.sym(Bool, X.le(WU.U64{m, 0}, r), Nat.is_le(SW.value(WU.U64{m, 0}), SW.value(r)), WA.le_value(WU.U64{m, 0}, r)), hc)
      +hle = L.subst(Nat, z => {Nat.is_le(z, SW.value(r)) == True{} : Bool}, SW.value(WU.U64{m, 0}), 1n+bp, hmv, hle0)
      +w = X.sub(r, WU.U64{m, 0})
      +es = Equal.trans(Nat, SW.value(w), Nat.sub(SW.value(r), SW.value(WU.U64{m, 0})), Nat.sub(SW.value(r), 1n+bp), WA.sub_value(r, WU.U64{m, 0}, hle0), Equal.cong(Nat, Nat, z => Nat.sub(SW.value(r), z), SW.value(WU.U64{m, 0}), 1n+bp, hmv))
      +x = Nat.sub(SW.value(r), 1n+bp)
      +hx = N.sub_lt(SW.value(r), 1n+bp, 1n+bp, hle, hr)
      +f = WW.fits_one(32n, one, h1, SW.value(w), L.subst(Nat, z => {Nat.is_lt(z, C.shift(32n, one)) == True{} : Bool}, x, SW.value(w), Equal.sym(Nat, SW.value(w), x, es), N.lt_trans(x, 1n+bp, C.shift(32n, one), hx, hm32)))
      +er = Equal.trans(Nat, Nat.add(Nat.mul(1n, 1n+bp), x), Nat.add(1n+bp, x), SW.value(r), Equal.cong(Nat, Nat, z => Nat.add(z, x), Nat.mul(1n, 1n+bp), 1n+bp, AQ.mul1(1n+bp)), N.sub_add(SW.value(r), 1n+bp, hle))
      +em = Equal.trans(Nat, Nat.mod(SW.value(r), 1n+bp), Nat.mod(Nat.add(Nat.mul(1n, 1n+bp), x), 1n+bp), x, Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), SW.value(r), Nat.add(Nat.mul(1n, 1n+bp), x), Equal.sym(Nat, Nat.add(Nat.mul(1n, 1n+bp), x), SW.value(r), er)), NR.mod_of(1n, bp, x, hx))
      Equal.trans(Nat, v(X.lo(w)), x, Nat.mod(SW.value(r), 1n+bp), Equal.trans(Nat, v(X.lo(w)), SW.value(w), x, lo32(w, f), es), Equal.sym(Nat, Nat.mod(SW.value(r), 1n+bp), x, em))
    case False{}:
      +hmv = Equal.trans(Nat, SW.value(WU.U64{m, 0}), v(m), 1n+bp, M128.val0(m), hM)
      +hm32 = WW.lt_one(32n, one, h1, 1n+bp, L.subst(Nat, z => {C.fits(32n, z) == True{} : Bool}, v(m), 1n+bp, hM, LW.vb(m)))
      +hle0 = Equal.trans(Bool, Nat.is_le(SW.value(WU.U64{m, 0}), SW.value(r)), X.le(WU.U64{m, 0}, r), False{}, Equal.sym(Bool, X.le(WU.U64{m, 0}, r), Nat.is_le(SW.value(WU.U64{m, 0}), SW.value(r)), WA.le_value(WU.U64{m, 0}, r)), hc)
      +hl = L.subst(Nat, z => {Nat.is_lt(SW.value(r), z) == True{} : Bool}, SW.value(WU.U64{m, 0}), 1n+bp, hmv, N.not_le_lt(SW.value(WU.U64{m, 0}), SW.value(r), hle0))
      +f = WW.fits_one(32n, one, h1, SW.value(r), N.lt_trans(SW.value(r), 1n+bp, C.shift(32n, one), hl, hm32))
      Equal.trans(Nat, v(X.lo(r)), SW.value(r), Nat.mod(SW.value(r), 1n+bp), lo32(r, f), Equal.sym(Nat, Nat.mod(SW.value(r), 1n+bp), SW.value(r), NR.mod_of(0n, bp, SW.value(r), hl)))

def sif(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +r: WU.U64, +hM: {v(m) == 1n+bp : Nat}, +hr: {Nat.is_lt(SW.value(r), Nat.add(1n+bp, 1n+bp)) == True{} : Bool}) -> {v(X.redc32_r(m, r)) == Nat.mod(SW.value(r), 1n+bp) : Nat}:
  sif_c(one, h1, bp, m, r, hM, hr, X.le(WU.U64{m, 0}, r), {==})


def rp_low(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +mp: U32, +hM: {v(m) == 1n+bp : Nat}, +hinv: {1n+C.low(32n, Nat.mul(1n+bp, v(mp))) == C.shift(32n, one) : Nat}, +t: WU.U64, +p: WU.U64, +eP: {Nat.add(v(X.lo(p)), C.shift(32n, v(X.hi(p)))) == Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp) : Nat}) -> {Nat.add(v(X.lo(t)), v(X.lo(p))) == C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))) : Nat}:
  +epl = Equal.trans(Nat, C.low(32n, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), C.low(32n, Nat.add(v(X.lo(p)), C.shift(32n, v(X.hi(p))))), v(X.lo(p)), Equal.cong(Nat, Nat, z => C.low(32n, z), Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp), Nat.add(v(X.lo(p)), C.shift(32n, v(X.hi(p)))), Equal.sym(Nat, Nat.add(v(X.lo(p)), C.shift(32n, v(X.hi(p)))), Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp), eP)), WW.low_u(32n, v(X.lo(p)), v(X.hi(p)), LW.vb(X.lo(p))))
  +e0 = Equal.trans(Nat, C.low(32n, Nat.add(v(X.lo(t)), v(X.lo(p)))), C.low(32n, Nat.add(v(X.lo(t)), C.low(32n, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)))), 0n, Equal.cong(Nat, Nat, z => C.low(32n, Nat.add(v(X.lo(t)), z)), v(X.lo(p)), C.low(32n, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), Equal.sym(Nat, C.low(32n, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), v(X.lo(p)), epl)), Equal.trans(Nat, C.low(32n, Nat.add(v(X.lo(t)), C.low(32n, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)))), C.low(32n, Nat.add(v(X.lo(t)), Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp))), 0n, MN.low_addlow(32n, v(X.lo(t)), Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), Equal.trans(Nat, C.low(32n, Nat.add(v(X.lo(t)), Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp))), C.low(32n, Nat.add(v(X.lo(t)), Nat.mul(C.low(32n, Nat.mul(v(X.lo(t)), v(mp))), 1n+bp))), 0n, Equal.cong(Nat, Nat, z => C.low(32n, Nat.add(v(X.lo(t)), Nat.mul(z, 1n+bp))), v(U32.mul(X.lo(t), mp)), C.low(32n, Nat.mul(v(X.lo(t)), v(mp))), SH.mul_low(X.lo(t), mp)), MN.redc0(32n, one, v(X.lo(t)), 1n+bp, v(mp), hinv))))
  +ea = Equal.trans(Nat, v(U32.add(X.lo(t), X.lo(p))), C.low(32n, Nat.add(v(X.lo(t)), v(X.lo(p)))), 0n, Equal.trans(Nat, v(U32.add(X.lo(t), X.lo(p))), C.low(32n, Nat.add(v(U32.add(X.lo(t), X.lo(p))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))))), C.low(32n, Nat.add(v(X.lo(t)), v(X.lo(p)))), Equal.sym(Nat, C.low(32n, Nat.add(v(U32.add(X.lo(t), X.lo(p))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))))), v(U32.add(X.lo(t), X.lo(p))), WW.low_u(32n, v(U32.add(X.lo(t), X.lo(p))), S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))), LW.vb(U32.add(X.lo(t), X.lo(p))))), Equal.cong(Nat, Nat, z => C.low(32n, z), Nat.add(v(U32.add(X.lo(t), X.lo(p))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), Nat.add(v(X.lo(t)), v(X.lo(p))), Equal.sym(Nat, Nat.add(v(X.lo(t)), v(X.lo(p))), Nat.add(v(U32.add(X.lo(t), X.lo(p))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), cadd(X.lo(t), X.lo(p))))), e0)
  Equal.trans(Nat, Nat.add(v(X.lo(t)), v(X.lo(p))), Nat.add(v(U32.add(X.lo(t), X.lo(p))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), cadd(X.lo(t), X.lo(p)), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), v(U32.add(X.lo(t), X.lo(p))), 0n, ea))

# 2^32 r' == t + u m for r' = s2 + 2^32 (c1 + c2)
def rp_eq(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +mp: U32, +hM: {v(m) == 1n+bp : Nat}, +hinv: {1n+C.low(32n, Nat.mul(1n+bp, v(mp))) == C.shift(32n, one) : Nat}, +t: WU.U64, +p: WU.U64, +T: Nat, +eT: {Nat.add(v(X.lo(t)), C.shift(32n, v(X.hi(t)))) == T : Nat}, +eP: {Nat.add(v(X.lo(p)), C.shift(32n, v(X.hi(p)))) == Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp) : Nat}) -> {C.shift(32n, Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))))) == Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)) : Nat}:
  +x1 = cadd(X.hi(t), X.hi(p))
  +x2 = Equal.trans(Nat, Nat.add(v(U32.add(X.hi(t), X.hi(p))), S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), Nat.add(v(U32.add(X.hi(t), X.hi(p))), v(X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))), Equal.cong(Nat, Nat, z => Nat.add(v(U32.add(X.hi(t), X.hi(p))), z), S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))), v(X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), Equal.sym(Nat, v(X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))), b32v(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), cadd(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))))
  Equal.trans(Nat, C.shift(32n, Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))))), Nat.add(C.shift(32n, v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))))), C.shift(32n, C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))))), Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), WW.shift_add(32n, v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))))), Equal.trans(Nat, Nat.add(C.shift(32n, v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))))), C.shift(32n, C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))))), Nat.add(C.shift(32n, v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))))), C.shift(32n, C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))), S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))))), Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), Equal.cong(Nat, Nat, z => Nat.add(C.shift(32n, v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))))), C.shift(32n, C.shift(32n, z))), Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))), Nat.add(S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))), S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t)))), NA.add_comm(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))), Equal.trans(Nat, Nat.add(C.shift(32n, v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))))), C.shift(32n, C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))), S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))))), Nat.add(C.shift(32n, v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))))), C.shift(32n, Nat.add(C.shift(32n, S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))))), Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), Equal.cong(Nat, Nat, z => Nat.add(C.shift(32n, v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))))), C.shift(32n, z)), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))), S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))), Nat.add(C.shift(32n, S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))), WW.shift_add(32n, S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))), S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))), Equal.trans(Nat, Nat.add(C.shift(32n, v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))))), C.shift(32n, Nat.add(C.shift(32n, S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))))), C.shift(32n, Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), Nat.add(C.shift(32n, S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))))), Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), Equal.sym(Nat, C.shift(32n, Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), Nat.add(C.shift(32n, S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))))), Nat.add(C.shift(32n, v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))))), C.shift(32n, Nat.add(C.shift(32n, S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))))), WW.shift_add(32n, v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), Nat.add(C.shift(32n, S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))))), Equal.trans(Nat, C.shift(32n, Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), Nat.add(C.shift(32n, S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))))), C.shift(32n, Nat.add(Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t)))))), Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), Equal.cong(Nat, Nat, z => C.shift(32n, z), Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), Nat.add(C.shift(32n, S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t)))))), Nat.add(Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))), Equal.sym(Nat, Nat.add(Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))), Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), Nat.add(C.shift(32n, S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t)))))), NA.add_assoc(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))))), Equal.trans(Nat, C.shift(32n, Nat.add(Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t)))))), C.shift(32n, Nat.add(Nat.add(v(U32.add(X.hi(t), X.hi(p))), S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t)))))), Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), Equal.cong(Nat, Nat, z => C.shift(32n, Nat.add(z, C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t)))))), Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))), Nat.add(v(U32.add(X.hi(t), X.hi(p))), S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), Equal.sym(Nat, Nat.add(v(U32.add(X.hi(t), X.hi(p))), S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))), x2)), Equal.trans(Nat, C.shift(32n, Nat.add(Nat.add(v(U32.add(X.hi(t), X.hi(p))), S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t)))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))), Nat.add(v(U32.add(X.hi(t), X.hi(p))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))))), Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), Equal.cong(Nat, Nat, z => C.shift(32n, z), Nat.add(Nat.add(v(U32.add(X.hi(t), X.hi(p))), S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))), Nat.add(S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))), Nat.add(v(U32.add(X.hi(t), X.hi(p))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t)))))), Equal.trans(Nat, Nat.add(Nat.add(v(U32.add(X.hi(t), X.hi(p))), S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))), Nat.add(Nat.add(S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))), v(U32.add(X.hi(t), X.hi(p)))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))), Nat.add(S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))), Nat.add(v(U32.add(X.hi(t), X.hi(p))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t)))))), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))), Nat.add(v(U32.add(X.hi(t), X.hi(p))), S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), Nat.add(S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))), v(U32.add(X.hi(t), X.hi(p)))), NA.add_comm(v(U32.add(X.hi(t), X.hi(p))), S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), NA.add_assoc(S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))), v(U32.add(X.hi(t), X.hi(p))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))))), Equal.trans(Nat, C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))), Nat.add(v(U32.add(X.hi(t), X.hi(p))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))), Nat.add(v(X.hi(t)), v(X.hi(p))))), Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), Equal.cong(Nat, Nat, z => C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))), z)), Nat.add(v(U32.add(X.hi(t), X.hi(p))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))), Nat.add(v(X.hi(t)), v(X.hi(p))), Equal.sym(Nat, Nat.add(v(X.hi(t)), v(X.hi(p))), Nat.add(v(U32.add(X.hi(t), X.hi(p))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))))), x1)), Equal.trans(Nat, C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))), Nat.add(v(X.hi(t)), v(X.hi(p))))), Nat.add(C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), C.shift(32n, Nat.add(v(X.hi(t)), v(X.hi(p))))), Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), WW.shift_add(32n, S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))), Nat.add(v(X.hi(t)), v(X.hi(p)))), Equal.trans(Nat, Nat.add(C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), C.shift(32n, Nat.add(v(X.hi(t)), v(X.hi(p))))), Nat.add(Nat.add(v(X.lo(t)), v(X.lo(p))), C.shift(32n, Nat.add(v(X.hi(t)), v(X.hi(p))))), Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, Nat.add(v(X.hi(t)), v(X.hi(p))))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), Nat.add(v(X.lo(t)), v(X.lo(p))), Equal.sym(Nat, Nat.add(v(X.lo(t)), v(X.lo(p))), C.shift(32n, S.bit_value(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), rp_low(one, h1, bp, m, mp, hM, hinv, t, p, eP))), Equal.trans(Nat, Nat.add(Nat.add(v(X.lo(t)), v(X.lo(p))), C.shift(32n, Nat.add(v(X.hi(t)), v(X.hi(p))))), Nat.add(Nat.add(v(X.lo(t)), v(X.lo(p))), Nat.add(C.shift(32n, v(X.hi(t))), C.shift(32n, v(X.hi(p))))), Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(v(X.lo(t)), v(X.lo(p))), z), C.shift(32n, Nat.add(v(X.hi(t)), v(X.hi(p)))), Nat.add(C.shift(32n, v(X.hi(t))), C.shift(32n, v(X.hi(p)))), WW.shift_add(32n, v(X.hi(t)), v(X.hi(p)))), Equal.trans(Nat, Nat.add(Nat.add(v(X.lo(t)), v(X.lo(p))), Nat.add(C.shift(32n, v(X.hi(t))), C.shift(32n, v(X.hi(p))))), Nat.add(Nat.add(v(X.lo(t)), C.shift(32n, v(X.hi(t)))), Nat.add(v(X.lo(p)), C.shift(32n, v(X.hi(p))))), Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), UM.swap4(v(X.lo(t)), v(X.lo(p)), C.shift(32n, v(X.hi(t))), C.shift(32n, v(X.hi(p)))), Equal.trans(Nat, Nat.add(Nat.add(v(X.lo(t)), C.shift(32n, v(X.hi(t)))), Nat.add(v(X.lo(p)), C.shift(32n, v(X.hi(p))))), Nat.add(T, Nat.add(v(X.lo(p)), C.shift(32n, v(X.hi(p))))), Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(v(X.lo(p)), C.shift(32n, v(X.hi(p))))), Nat.add(v(X.lo(t)), C.shift(32n, v(X.hi(t)))), T, eT), Equal.cong(Nat, Nat, z => Nat.add(T, z), Nat.add(v(X.lo(p)), C.shift(32n, v(X.hi(p)))), Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp), eP))))))))))))))

# r' < 2 m for t < m^2 and m < 2^32
# over an open bound b (1 + bp at the use): a closed-width shift of 1 + bp
# would be unfolded into 2^32 successors
def rp_lt_g(+one: Nat, +h1: {one == 1n : Nat}, +b: Nat, +hb: {Nat.is_lt(0n, b) == True{} : Bool}, +hbf: {C.fits(32n, b) == True{} : Bool}, +t: WU.U64, +mp: U32, +T: Nat, +hT: {Nat.is_lt(T, Nat.mul(b, b)) == True{} : Bool}, +R: Nat, +er: {C.shift(32n, R) == Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), b)) : Nat}) -> {Nat.is_lt(R, Nat.add(b, b)) == True{} : Bool}:
  +hm32 = WW.lt_one(32n, one, h1, b, hbf)
  +a1 = AQ.mle2(b, b, b, C.shift(32n, one), N.le_refl(b), N.lt_le(b, C.shift(32n, one), hm32))
  +a2 = L.subst(Nat, z => {Nat.is_le(Nat.mul(b, b), z) == True{} : Bool}, Nat.mul(b, C.shift(32n, one)), C.shift(32n, b), Equal.sym(Nat, C.shift(32n, b), Nat.mul(b, C.shift(32n, one)), WW.shift_mul_one(32n, one, h1, b)), a1)
  +hT2 = N.lt_le_trans(T, Nat.mul(b, b), C.shift(32n, b), hT, a2)
  +hU = WW.lt_one(32n, one, h1, v(U32.mul(X.lo(t), mp)), LW.vb(U32.mul(X.lo(t), mp)))
  +b1 = AQ.mle2(1n+v(U32.mul(X.lo(t), mp)), C.shift(32n, one), b, b, N.lt_succ_le_succ(v(U32.mul(X.lo(t), mp)), C.shift(32n, one), hU), N.le_refl(b))
  +b2 = L.subst(Nat, z => {Nat.is_le(Nat.mul(1n+v(U32.mul(X.lo(t), mp)), b), z) == True{} : Bool}, Nat.mul(C.shift(32n, one), b), C.shift(32n, b), Equal.trans(Nat, Nat.mul(C.shift(32n, one), b), Nat.mul(b, C.shift(32n, one)), C.shift(32n, b), NA.mul_comm(C.shift(32n, one), b), Equal.sym(Nat, C.shift(32n, b), Nat.mul(b, C.shift(32n, one)), WW.shift_mul_one(32n, one, h1, b))), b1)
  +b3 = L.subst(Nat, z => {Nat.is_lt(Nat.mul(v(U32.mul(X.lo(t), mp)), b), z) == True{} : Bool}, Nat.add(Nat.mul(v(U32.mul(X.lo(t), mp)), b), b), Nat.add(b, Nat.mul(v(U32.mul(X.lo(t), mp)), b)), NA.add_comm(Nat.mul(v(U32.mul(X.lo(t), mp)), b), b), DM.lt_add_pos(Nat.mul(v(U32.mul(X.lo(t), mp)), b), b, hb))
  +hUM = N.lt_le(Nat.mul(v(U32.mul(X.lo(t), mp)), b), C.shift(32n, b), N.lt_le_trans(Nat.mul(v(U32.mul(X.lo(t), mp)), b), Nat.mul(1n+v(U32.mul(X.lo(t), mp)), b), C.shift(32n, b), b3, b2))
  +c1 = SQ2.le_add2(1n+T, C.shift(32n, b), Nat.mul(v(U32.mul(X.lo(t), mp)), b), C.shift(32n, b), N.lt_succ_le_succ(T, C.shift(32n, b), hT2), hUM)
  +c2 = N.succ_le_lt(Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), b)), Nat.add(C.shift(32n, b), C.shift(32n, b)), c1)
  +c3 = L.subst(Nat, z => {Nat.is_lt(Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), b)), z) == True{} : Bool}, Nat.add(C.shift(32n, b), C.shift(32n, b)), C.shift(32n, Nat.add(b, b)), Equal.sym(Nat, C.shift(32n, Nat.add(b, b)), Nat.add(C.shift(32n, b), C.shift(32n, b)), WW.shift_add(32n, b, b)), c2)
  +c4 = L.subst(Nat, z => {Nat.is_lt(z, C.shift(32n, Nat.add(b, b))) == True{} : Bool}, Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), b)), C.shift(32n, R), Equal.sym(Nat, C.shift(32n, R), Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), b)), er), c3)
  UM.shl_inv(32n, R, Nat.add(b, b), c4)

def rp_lt(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +mp: U32, +hM: {v(m) == 1n+bp : Nat}, +hinv: {1n+C.low(32n, Nat.mul(1n+bp, v(mp))) == C.shift(32n, one) : Nat}, +t: WU.U64, +p: WU.U64, +T: Nat, +eT: {Nat.add(v(X.lo(t)), C.shift(32n, v(X.hi(t)))) == T : Nat}, +hT: {Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}, +eP: {Nat.add(v(X.lo(p)), C.shift(32n, v(X.hi(p)))) == Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp) : Nat}) -> {Nat.is_lt(Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))))), Nat.add(1n+bp, 1n+bp)) == True{} : Bool}:
  rp_lt_g(one, h1, 1n+bp, {==}, L.subst(Nat, z => {C.fits(32n, z) == True{} : Bool}, v(m), 1n+bp, hM, LW.vb(m)), t, mp, T, hT, Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))))), rp_eq(one, h1, bp, m, mp, hM, hinv, t, p, T, eT, eP))

def r_v(+t: WU.U64, +p: WU.U64) -> {SW.value(WU.U64{U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.b32(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), X.b32(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))}) == Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))))) : Nat}:
  Equal.cong(Nat, Nat, z => Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, z)), v(U32.add(X.b32(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), X.b32(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))), Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))), kv(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t)), U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))

# redc32_p is r' mod m
def rp_mod(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +mp: U32, +hM: {v(m) == 1n+bp : Nat}, +hinv: {1n+C.low(32n, Nat.mul(1n+bp, v(mp))) == C.shift(32n, one) : Nat}, +t: WU.U64, +p: WU.U64, +T: Nat, +eT: {Nat.add(v(X.lo(t)), C.shift(32n, v(X.hi(t)))) == T : Nat}, +hT: {Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}, +eP: {Nat.add(v(X.lo(p)), C.shift(32n, v(X.hi(p)))) == Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp) : Nat}) -> {v(X.redc32_p(m, t, p)) == Nat.mod(Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))))), 1n+bp) : Nat}:
  +hr = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(1n+bp, 1n+bp)) == True{} : Bool}, Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))))), SW.value(WU.U64{U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.b32(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), X.b32(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))}), Equal.sym(Nat, SW.value(WU.U64{U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.b32(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), X.b32(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))}), Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))))), r_v(t, p)), rp_lt(one, h1, bp, m, mp, hM, hinv, t, p, T, eT, hT, eP))
  Equal.trans(Nat, v(X.redc32_p(m, t, p)), Nat.mod(SW.value(WU.U64{U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.b32(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), X.b32(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))}), 1n+bp), Nat.mod(Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))))), 1n+bp), sif(one, h1, bp, m, WU.U64{U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.b32(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), X.b32(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))}, hM, hr), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), SW.value(WU.U64{U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.b32(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), X.b32(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))}), Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))))), r_v(t, p)))

def rp_lt_m(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +mp: U32, +hM: {v(m) == 1n+bp : Nat}, +hinv: {1n+C.low(32n, Nat.mul(1n+bp, v(mp))) == C.shift(32n, one) : Nat}, +t: WU.U64, +p: WU.U64, +T: Nat, +eT: {Nat.add(v(X.lo(t)), C.shift(32n, v(X.hi(t)))) == T : Nat}, +hT: {Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}, +eP: {Nat.add(v(X.lo(p)), C.shift(32n, v(X.hi(p)))) == Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp) : Nat}) -> {Nat.is_lt(v(X.redc32_p(m, t, p)), 1n+bp) == True{} : Bool}:
  L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))))), 1n+bp), v(X.redc32_p(m, t, p)), Equal.sym(Nat, v(X.redc32_p(m, t, p)), Nat.mod(Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))))), 1n+bp), rp_mod(one, h1, bp, m, mp, hM, hinv, t, p, T, eT, hT, eP)), NR.dm_lt(bp, Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))))))

def rp_cong(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +mp: U32, +hM: {v(m) == 1n+bp : Nat}, +hinv: {1n+C.low(32n, Nat.mul(1n+bp, v(mp))) == C.shift(32n, one) : Nat}, +t: WU.U64, +p: WU.U64, +T: Nat, +eT: {Nat.add(v(X.lo(t)), C.shift(32n, v(X.hi(t)))) == T : Nat}, +hT: {Nat.is_lt(T, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}, +eP: {Nat.add(v(X.lo(p)), C.shift(32n, v(X.hi(p)))) == Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp) : Nat}) -> {Nat.mod(C.shift(32n, v(X.redc32_p(m, t, p))), 1n+bp) == Nat.mod(T, 1n+bp) : Nat}:
  Equal.trans(Nat, Nat.mod(C.shift(32n, v(X.redc32_p(m, t, p))), 1n+bp), Nat.mod(C.shift(32n, Nat.mod(Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))))), 1n+bp)), 1n+bp), Nat.mod(T, 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(C.shift(32n, z), 1n+bp), v(X.redc32_p(m, t, p)), Nat.mod(Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))))), 1n+bp), rp_mod(one, h1, bp, m, mp, hM, hinv, t, p, T, eT, hT, eP)), Equal.trans(Nat, Nat.mod(C.shift(32n, Nat.mod(Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p))))))), 1n+bp)), 1n+bp), Nat.mod(C.shift(32n, Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))))), 1n+bp), Nat.mod(T, 1n+bp), MN.mod_shift(bp, 32n, Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))))), Equal.trans(Nat, Nat.mod(C.shift(32n, Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))))), 1n+bp), Nat.mod(Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), 1n+bp), Nat.mod(T, 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), C.shift(32n, Nat.add(v(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t))))), C.shift(32n, Nat.add(S.bit_value(U32.is_lt(U32.add(X.hi(t), X.hi(p)), X.hi(t))), S.bit_value(U32.is_lt(U32.add(U32.add(X.hi(t), X.hi(p)), X.b32(U32.is_lt(U32.add(X.lo(t), X.lo(p)), X.lo(t)))), U32.add(X.hi(t), X.hi(p)))))))), Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), rp_eq(one, h1, bp, m, mp, hM, hinv, t, p, T, eT, eP)), Equal.trans(Nat, Nat.mod(Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), 1n+bp), Nat.mod(Nat.add(Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp), T), 1n+bp), Nat.mod(T, 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.add(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp)), Nat.add(Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp), T), NA.add_comm(T, Nat.mul(v(U32.mul(X.lo(t), mp)), 1n+bp))), NR.absorb(bp, v(U32.mul(X.lo(t), mp)), T)))))

def ep_m(+bp: Nat, +m: U32, +hM: {v(m) == 1n+bp : Nat}, +u: U32) -> {Nat.add(v(X.lo(X.mul32(u, m))), C.shift(32n, v(X.hi(X.mul32(u, m))))) == Nat.mul(v(u), 1n+bp) : Nat}:
  Equal.trans(Nat, Nat.add(v(X.lo(X.mul32(u, m))), C.shift(32n, v(X.hi(X.mul32(u, m))))), Nat.mul(v(u), v(m)), Nat.mul(v(u), 1n+bp), m32v(u, m), Equal.cong(Nat, Nat, z => Nat.mul(v(u), z), v(m), 1n+bp, hM))

def ab_lt(+bp: Nat, +a: Nat, +b: Nat, +ha: {Nat.is_lt(a, 1n+bp) == True{} : Bool}, +hb: {Nat.is_lt(b, 1n+bp) == True{} : Bool}) -> {Nat.is_lt(Nat.mul(a, b), Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}:
  UM.ab_lt(bp, a, b, ha, hb)

# 32-bit Montgomery multiplication: mont32(a, b) < m and mont32(a, b) 2^32 == a b (mod m)
def mont_lt(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +mp: U32, +hM: {v(m) == 1n+bp : Nat}, +hinv: {1n+C.low(32n, Nat.mul(1n+bp, v(mp))) == C.shift(32n, one) : Nat}, +a: U32, +b: U32, +hT: {Nat.is_lt(Nat.mul(v(a), v(b)), Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}) -> {Nat.is_lt(v(X.mont32(m, mp, a, b)), 1n+bp) == True{} : Bool}:
  rp_lt_m(one, h1, bp, m, mp, hM, hinv, X.mul32(a, b), X.mul32(U32.mul(X.lo(X.mul32(a, b)), mp), m), Nat.mul(v(a), v(b)), m32v(a, b), hT, ep_m(bp, m, hM, U32.mul(X.lo(X.mul32(a, b)), mp)))

def mont_cong(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +mp: U32, +hM: {v(m) == 1n+bp : Nat}, +hinv: {1n+C.low(32n, Nat.mul(1n+bp, v(mp))) == C.shift(32n, one) : Nat}, +a: U32, +b: U32, +hT: {Nat.is_lt(Nat.mul(v(a), v(b)), Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}) -> {Nat.mod(C.shift(32n, v(X.mont32(m, mp, a, b))), 1n+bp) == Nat.mod(Nat.mul(v(a), v(b)), 1n+bp) : Nat}:
  rp_cong(one, h1, bp, m, mp, hM, hinv, X.mul32(a, b), X.mul32(U32.mul(X.lo(X.mul32(a, b)), mp), m), Nat.mul(v(a), v(b)), m32v(a, b), hT, ep_m(bp, m, hM, U32.mul(X.lo(X.mul32(a, b)), mp)))


def mlt(+bp: Nat, +x: Nat) -> {Nat.is_lt(Nat.mod(x, 1n+bp), 1n+bp) == True{} : Bool}:
  NR.dm_lt(bp, x)

def smul(+x: Nat, +y: Nat) -> {Nat.mul(C.shift(32n, x), C.shift(32n, y)) == C.shift(32n, C.shift(32n, Nat.mul(x, y))) : Nat}:
  Equal.trans(Nat, Nat.mul(C.shift(32n, x), C.shift(32n, y)), C.shift(32n, Nat.mul(x, C.shift(32n, y))), C.shift(32n, C.shift(32n, Nat.mul(x, y))), WW.shift_mul_l(32n, x, C.shift(32n, y)), Equal.cong(Nat, Nat, z => C.shift(32n, z), Nat.mul(x, C.shift(32n, y)), C.shift(32n, Nat.mul(x, y)), WW.shift_mul_r(32n, x, y)))

def mform(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +mp: U32, +hM: {v(m) == 1n+bp : Nat}, +hinv: {1n+C.low(32n, Nat.mul(1n+bp, v(mp))) == C.shift(32n, one) : Nat}, +hh: Nat, +hH: {1n+1n+bp == Nat.add(hh, hh) : Nat}, +a: U32, +b: U32, +an: Nat, +bn: Nat, +ha: {v(a) == Nat.mod(C.shift(32n, an), 1n+bp) : Nat}, +hb: {v(b) == Nat.mod(C.shift(32n, bn), 1n+bp) : Nat}) -> {v(X.mont32(m, mp, a, b)) == Nat.mod(C.shift(32n, Nat.mod(Nat.mul(an, bn), 1n+bp)), 1n+bp) : Nat}:
  +la = L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(C.shift(32n, an), 1n+bp), v(a), Equal.sym(Nat, v(a), Nat.mod(C.shift(32n, an), 1n+bp), ha), mlt(bp, C.shift(32n, an)))
  +lb = L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(C.shift(32n, bn), 1n+bp), v(b), Equal.sym(Nat, v(b), Nat.mod(C.shift(32n, bn), 1n+bp), hb), mlt(bp, C.shift(32n, bn)))
  +o = v(X.mont32(m, mp, a, b))
  +e1 = Equal.trans(Nat, Nat.mod(C.shift(32n, o), 1n+bp), Nat.mod(Nat.mul(v(a), v(b)), 1n+bp), Nat.mod(C.shift(32n, C.shift(32n, Nat.mul(an, bn))), 1n+bp), mont_cong(one, h1, bp, m, mp, hM, hinv, a, b, ab_lt(bp, v(a), v(b), la, lb)), Equal.trans(Nat, Nat.mod(Nat.mul(v(a), v(b)), 1n+bp), Nat.mod(Nat.mul(Nat.mod(C.shift(32n, an), 1n+bp), v(b)), 1n+bp), Nat.mod(C.shift(32n, C.shift(32n, Nat.mul(an, bn))), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(Nat.mul(z, v(b)), 1n+bp), v(a), Nat.mod(C.shift(32n, an), 1n+bp), ha), Equal.trans(Nat, Nat.mod(Nat.mul(Nat.mod(C.shift(32n, an), 1n+bp), v(b)), 1n+bp), Nat.mod(Nat.mul(Nat.mod(C.shift(32n, an), 1n+bp), Nat.mod(C.shift(32n, bn), 1n+bp)), 1n+bp), Nat.mod(C.shift(32n, C.shift(32n, Nat.mul(an, bn))), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(Nat.mul(Nat.mod(C.shift(32n, an), 1n+bp), z), 1n+bp), v(b), Nat.mod(C.shift(32n, bn), 1n+bp), hb), Equal.trans(Nat, Nat.mod(Nat.mul(Nat.mod(C.shift(32n, an), 1n+bp), Nat.mod(C.shift(32n, bn), 1n+bp)), 1n+bp), Nat.mod(Nat.mul(C.shift(32n, an), Nat.mod(C.shift(32n, bn), 1n+bp)), 1n+bp), Nat.mod(C.shift(32n, C.shift(32n, Nat.mul(an, bn))), 1n+bp), NR.mod_mul_l(bp, C.shift(32n, an), Nat.mod(C.shift(32n, bn), 1n+bp)), Equal.trans(Nat, Nat.mod(Nat.mul(C.shift(32n, an), Nat.mod(C.shift(32n, bn), 1n+bp)), 1n+bp), Nat.mod(Nat.mul(C.shift(32n, an), C.shift(32n, bn)), 1n+bp), Nat.mod(C.shift(32n, C.shift(32n, Nat.mul(an, bn))), 1n+bp), NR.mod_mul_r(bp, C.shift(32n, an), C.shift(32n, bn)), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.mul(C.shift(32n, an), C.shift(32n, bn)), C.shift(32n, C.shift(32n, Nat.mul(an, bn))), smul(an, bn)))))))
  +e2 = MN.cancel(bp, hh, hH, 32n, o, C.shift(32n, Nat.mul(an, bn)), e1)
  +lo = mont_lt(one, h1, bp, m, mp, hM, hinv, a, b, ab_lt(bp, v(a), v(b), la, lb))
  +e3 = Equal.sym(Nat, Nat.mod(o, 1n+bp), o, NR.mod_of(0n, bp, o, lo))
  Equal.trans(Nat, o, Nat.mod(o, 1n+bp), Nat.mod(C.shift(32n, Nat.mod(Nat.mul(an, bn), 1n+bp)), 1n+bp), e3, Equal.trans(Nat, Nat.mod(o, 1n+bp), Nat.mod(C.shift(32n, Nat.mul(an, bn)), 1n+bp), Nat.mod(C.shift(32n, Nat.mod(Nat.mul(an, bn), 1n+bp)), 1n+bp), e2, Equal.sym(Nat, Nat.mod(C.shift(32n, Nat.mod(Nat.mul(an, bn), 1n+bp)), 1n+bp), Nat.mod(C.shift(32n, Nat.mul(an, bn)), 1n+bp), MN.mod_shift(bp, 32n, Nat.mul(an, bn)))))

def mbit_v(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +mp: U32, +hM: {v(m) == 1n+bp : Nat}, +hinv: {1n+C.low(32n, Nat.mul(1n+bp, v(mp))) == C.shift(32n, one) : Nat}, +hh: Nat, +hH: {1n+1n+bp == Nat.add(hh, hh) : Nat}, +b: U32, +acc: U32, +bn: Nat, +an: Nat, +hb: {v(b) == Nat.mod(C.shift(32n, bn), 1n+bp) : Nat}, +ha: {v(acc) == Nat.mod(C.shift(32n, an), 1n+bp) : Nat}, +d: Nat, +o: Bool, +hd: {Nat.is_lt(d, 2n) == True{} : Bool}, +ho: {o == Nat.is_eq(d, 1n) : Bool}) -> {v(X.mbit32(o, m, mp, b, acc)) == Nat.mod(C.shift(32n, M.pow_mod_odd(1n+bp, d, bn, an)), 1n+bp) : Nat}:
  match d o:
    case 0n False{}:
      ha
    case 0n True{}:
      Empty.absurd({v(X.mbit32(True{}, m, mp, b, acc)) == Nat.mod(C.shift(32n, M.pow_mod_odd(1n+bp, 0n, bn, an)), 1n+bp) : Nat}, true_ne_false(ho))
    case 1n True{}:
      mform(one, h1, bp, m, mp, hM, hinv, hh, hH, acc, b, an, bn, ha, hb)
    case 1n False{}:
      Empty.absurd({v(X.mbit32(False{}, m, mp, b, acc)) == Nat.mod(C.shift(32n, M.pow_mod_odd(1n+bp, 1n, bn, an)), 1n+bp) : Nat}, true_ne_false(Equal.sym(Bool, False{}, True{}, ho)))
    case 2n+q _:
      Empty.absurd({v(X.mbit32(o, m, mp, b, acc)) == Nat.mod(C.shift(32n, M.pow_mod_odd(1n+bp, 2n+q, bn, an)), 1n+bp) : Nat}, N.lt_zero_absurd(q, hd))

def izv(+a: U32, +n: Nat, +h: {v(a) == n : Nat}) -> {U32.is_zero(a) == Nat.is_eq(n, 0n) : Bool}:
  Equal.trans(Bool, U32.is_zero(a), Nat.is_eq(v(a), 0n), Nat.is_eq(n, 0n), LW.tests_is_zero(a), Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), v(a), n, h))

def msim(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +mp: U32, +hM: {v(m) == 1n+bp : Nat}, +hinv: {1n+C.low(32n, Nat.mul(1n+bp, v(mp))) == C.shift(32n, one) : Nat}, +hh: Nat, +hH: {1n+1n+bp == Nat.add(hh, hh) : Nat}, +f: Nat, +b: U32, +acc: U32, +e: U32, +bn: Nat, +an: Nat, +hb: {v(b) == Nat.mod(C.shift(32n, bn), 1n+bp) : Nat}, +ha: {v(acc) == Nat.mod(C.shift(32n, an), 1n+bp) : Nat}, +ez: Bool, +ne: Nat, +hez: {U32.is_zero(e) == ez : Bool}, +hne: {v(e) == ne : Nat}) -> {v(X.mpow32_go(f, m, mp, b, acc, (e, ez))) == Nat.mod(C.shift(32n, M.pow_mod_go(f, 1n+bp, ne, bn, an)), 1n+bp) : Nat}:
  match f ez ne:
    case 0n _ _:
      ha
    case 1n+g True{} 0n:
      ha
    case 1n+g True{} 1n+ep:
      Empty.absurd({v(X.mpow32_go(1n+g, m, mp, b, acc, (e, True{}))) == Nat.mod(C.shift(32n, M.pow_mod_go(1n+g, 1n+bp, 1n+ep, bn, an)), 1n+bp) : Nat}, true_ne_false(Equal.trans(Bool, True{}, U32.is_zero(e), False{}, Equal.sym(Bool, U32.is_zero(e), True{}, hez), izv(e, 1n+ep, hne))))
    case 1n+g False{} 0n:
      Empty.absurd({v(X.mpow32_go(1n+g, m, mp, b, acc, (e, False{}))) == Nat.mod(C.shift(32n, M.pow_mod_go(1n+g, 1n+bp, 0n, bn, an)), 1n+bp) : Nat}, true_ne_false(Equal.trans(Bool, True{}, U32.is_zero(e), False{}, Equal.sym(Bool, U32.is_zero(e), True{}, izv(e, 0n, hne)), hez)))
    case 1n+ +g False{} 1n+ +ep:
      +b2 = X.mont32(m, mp, b, b)
      +eb2 = mform(one, h1, bp, m, mp, hM, hinv, hh, hH, b, b, bn, bn, hb, hb)
      +o = U32.is_eq(U32.and(e, 1), 1)
      +d = Nat.mod(1n+ep, 2n)
      +ho = Equal.trans(Bool, o, Nat.is_eq(Nat.mod(v(e), 2n), 1n), Nat.is_eq(d, 1n), LW.tests_odd(e), Equal.cong(Nat, Bool, t => Nat.is_eq(Nat.mod(t, 2n), 1n), v(e), 1n+ep, hne))
      +a2 = X.mbit32(o, m, mp, b, acc)
      +ea2 = mbit_v(one, h1, bp, m, mp, hM, hinv, hh, hH, b, acc, bn, an, hb, ha, d, o, NR.dm_lt(1n, 1n+ep), ho)
      +e2 = U32.shr(e)
      +ee2 = Equal.trans(Nat, v(e2), Nat.div(v(e), 2n), Nat.div(1n+ep, 2n), LW.ops_half(e), Equal.cong(Nat, Nat, t => Nat.div(t, 2n), v(e), 1n+ep, hne))
      msim(one, h1, bp, m, mp, hM, hinv, hh, hH, g, b2, a2, e2, Nat.mod(Nat.mul(bn, bn), 1n+bp), M.pow_mod_odd(1n+bp, d, bn, an), eb2, ea2, U32.is_zero(e2), Nat.div(1n+ep, 2n), {==}, ee2)

def hdz(+bp: Nat, +m: U32, +hM: {v(m) == 1n+bp : Nat}) -> {U32.is_zero(m) == False{} : Bool}:
  Equal.trans(Bool, U32.is_zero(m), Nat.is_eq(v(m), 0n), False{}, LW.zero_nat(m), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), v(m), 1n+bp, hM))

# x 2^32 mod m by one 64 / 32 reduction
def to_mont_v(+bp: Nat, +m: U32, +hM: {v(m) == 1n+bp : Nat}, +x: U32) -> {v(X.mod32(WU.U64{0, x}, m)) == Nat.mod(C.shift(32n, v(x)), 1n+bp) : Nat}:
  Equal.trans(Nat, v(X.mod32(WU.U64{0, x}, m)), Nat.mod(SW.value(WU.U64{0, x}), v(m)), Nat.mod(C.shift(32n, v(x)), 1n+bp), W64D.mod32_value(WU.U64{0, x}, m, hdz(bp, m, hM)), Equal.cong(Nat, Nat, z => Nat.mod(C.shift(32n, v(x)), z), v(m), 1n+bp, hM))


# x 1 < m m for x < m
def g1_lt(+bp: Nat, +x: Nat, +h: {Nat.is_lt(x, 1n+bp) == True{} : Bool}) -> {Nat.is_lt(Nat.mul(x, v(1)), Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}:
  +e = NA.mul_one(x)
  +h2 = N.lt_le_trans(x, 1n+bp, Nat.mul(1n+bp, 1n+bp), h, L.subst(Nat, z => {Nat.is_le(1n+bp, z) == True{} : Bool}, Nat.add(1n+bp, Nat.mul(1n+bp, bp)), Nat.mul(1n+bp, 1n+bp), Equal.sym(Nat, Nat.mul(1n+bp, 1n+bp), Nat.add(1n+bp, Nat.mul(1n+bp, bp)), NA.mul_succ(1n+bp, bp)), N.le_add_right(1n+bp, Nat.mul(1n+bp, bp))))
  L.subst(Nat, z => {Nat.is_lt(z, Nat.mul(1n+bp, 1n+bp)) == True{} : Bool}, x, Nat.mul(x, v(1)), Equal.sym(Nat, Nat.mul(x, v(1)), x, e), h2)

def mpow_v(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +mp: U32, +hM: {v(m) == 1n+bp : Nat}, +hinv: {1n+C.low(32n, Nat.mul(1n+bp, v(mp))) == C.shift(32n, one) : Nat}, +b: U32, +hb: {Nat.is_lt(v(b), 1n+bp) == True{} : Bool}, +e: U32, +hodd: {Nat.mod(1n+bp, 2n) == 1n : Nat}) -> {v(X.mpow32_m(b, e, m, mp)) == M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp)) : Nat}:
  +hh : Nat = 1n+Nat.div(1n+bp, 2n)
  +hH = MN.odd_hh(bp, hodd)
  +bt = X.mod32(WU.U64{0, b}, m)
  +eb = to_mont_v(bp, m, hM, b)
  +o1 = U32.mod(1, m)
  +eo = Equal.trans(Nat, v(o1), Nat.mod(v(1), v(m)), Nat.mod(1n, 1n+bp), UD.mod_nat(1, m, hdz(bp, m, hM)), Equal.cong(Nat, Nat, z => Nat.mod(1n, z), v(m), 1n+bp, hM))
  +at = X.mod32(WU.U64{0, o1}, m)
  +ea = Equal.trans(Nat, v(at), Nat.mod(C.shift(32n, v(o1)), 1n+bp), Nat.mod(C.shift(32n, Nat.mod(1n, 1n+bp)), 1n+bp), to_mont_v(bp, m, hM, o1), Equal.cong(Nat, Nat, z => Nat.mod(C.shift(32n, z), 1n+bp), v(o1), Nat.mod(1n, 1n+bp), eo))
  +go = X.mpow32_go(140n, m, mp, bt, at, (e, U32.is_zero(e)))
  +eg = msim(one, h1, bp, m, mp, hM, hinv, hh, hH, 140n, bt, at, e, v(b), Nat.mod(1n, 1n+bp), eb, ea, U32.is_zero(e), v(e), {==}, {==})
  +lg = L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(C.shift(32n, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp))), 1n+bp), v(go), Equal.sym(Nat, v(go), Nat.mod(C.shift(32n, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp))), 1n+bp), eg), mlt(bp, C.shift(32n, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp)))))
  +hT1 = g1_lt(bp, v(go), lg)
  +o = v(X.mont32(m, mp, go, 1))
  +c1 = Equal.trans(Nat, Nat.mod(C.shift(32n, o), 1n+bp), Nat.mod(Nat.mul(v(go), v(1)), 1n+bp), Nat.mod(C.shift(32n, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp))), 1n+bp), mont_cong(one, h1, bp, m, mp, hM, hinv, go, 1, hT1), Equal.trans(Nat, Nat.mod(Nat.mul(v(go), v(1)), 1n+bp), Nat.mod(Nat.mul(v(go), 1n), 1n+bp), Nat.mod(C.shift(32n, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp))), 1n+bp), {==}, Equal.trans(Nat, Nat.mod(Nat.mul(v(go), 1n), 1n+bp), Nat.mod(v(go), 1n+bp), Nat.mod(C.shift(32n, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp))), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.mul(v(go), 1n), v(go), NA.mul_one(v(go))), Equal.trans(Nat, Nat.mod(v(go), 1n+bp), Nat.mod(Nat.mod(C.shift(32n, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp))), 1n+bp), 1n+bp), Nat.mod(C.shift(32n, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp))), 1n+bp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), v(go), Nat.mod(C.shift(32n, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp))), 1n+bp), eg), NR.mod_mod(bp, C.shift(32n, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp))))))))
  +c2 = MN.cancel(bp, hh, hH, 32n, o, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp)), c1)
  +lo = mont_lt(one, h1, bp, m, mp, hM, hinv, go, 1, hT1)
  +hP = UM.pm_lt(bp, 140n, v(e), v(b), Nat.mod(1n, 1n+bp), mlt(bp, 1n))
  Equal.trans(Nat, o, Nat.mod(o, 1n+bp), M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp)), Equal.sym(Nat, Nat.mod(o, 1n+bp), o, NR.mod_of(0n, bp, o, lo)), Equal.trans(Nat, Nat.mod(o, 1n+bp), Nat.mod(M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp)), 1n+bp), M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp)), c2, NR.mod_of(0n, bp, M.pow_mod_go(140n, 1n+bp, v(e), v(b), Nat.mod(1n, 1n+bp)), hP)))


def mok_odd(+bp: Nat, +m: U32, +hM: {v(m) == 1n+bp : Nat}, +hok: {X.mont32_ok(m) == True{} : Bool}) -> {Nat.mod(1n+bp, 2n) == 1n : Nat}:
  +h = Equal.trans(Bool, Nat.is_eq(Nat.mod(v(m), 2n), 1n), U32.is_eq(U32.and(m, 1), 1), True{}, Equal.sym(Bool, U32.is_eq(U32.and(m, 1), 1), Nat.is_eq(Nat.mod(v(m), 2n), 1n), LW.tests_odd(m)), W64S.and_l(U32.is_eq(U32.and(m, 1), 1), U32.is_eq(U32.mul(m, X.minv32(m)), 4294967295), hok))
  Equal.trans(Nat, Nat.mod(1n+bp, 2n), Nat.mod(v(m), 2n), 1n, Equal.cong(Nat, Nat, z => Nat.mod(z, 2n), 1n+bp, v(m), Equal.sym(Nat, v(m), 1n+bp, hM)), N.eq_from_is_eq(Nat.mod(v(m), 2n), 1n, h))

# over an open all-ones word o (a literal 2^32 - 1 is expanded in unary)
def mok_inv_o(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +hM: {v(m) == 1n+bp : Nat}, +o: U32, +po: {o == U32{WD.mask(32n, 32n)} : U32}, +heq: {U32.is_eq(U32.mul(m, X.minv32(m)), o) == True{} : Bool}) -> {1n+C.low(32n, Nat.mul(1n+bp, v(X.minv32(m)))) == C.shift(32n, one) : Nat}:
  +mp = X.minv32(m)
  +w = U32.mul(m, mp)
  +h = Equal.trans(Bool, Nat.is_eq(v(w), v(o)), U32.is_eq(U32.mul(m, X.minv32(m)), o), True{}, Equal.sym(Bool, U32.is_eq(U32.mul(m, X.minv32(m)), o), Nat.is_eq(v(w), v(o)), LW.eq_nat(w, o)), heq)
  +e1 = N.eq_from_is_eq(v(w), v(o), h)
  +e2 = Equal.trans(Nat, C.low(32n, Nat.mul(1n+bp, v(mp))), C.low(32n, Nat.mul(v(m), v(mp))), v(w), Equal.cong(Nat, Nat, z => C.low(32n, Nat.mul(z, v(mp))), 1n+bp, v(m), Equal.sym(Nat, v(m), 1n+bp, hM)), Equal.sym(Nat, v(w), C.low(32n, Nat.mul(v(m), v(mp))), SH.mul_low(m, mp)))
  +e3 = Equal.trans(Nat, 1n+v(o), WD.sc(32n, one), C.shift(32n, one), W64S.mask_v(32n, {==}, one, h1, o, po), Equal.sym(Nat, C.shift(32n, one), WD.sc(32n, one), W64M.shift_sc(32n, one)))
  Equal.trans(Nat, 1n+C.low(32n, Nat.mul(1n+bp, v(mp))), 1n+v(o), C.shift(32n, one), Equal.cong(Nat, Nat, z => 1n+z, C.low(32n, Nat.mul(1n+bp, v(mp))), v(o), Equal.trans(Nat, C.low(32n, Nat.mul(1n+bp, v(mp))), v(w), v(o), e2, e1)), e3)

def mok_inv(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +hM: {v(m) == 1n+bp : Nat}, +hok: {X.mont32_ok(m) == True{} : Bool}) -> {1n+C.low(32n, Nat.mul(1n+bp, v(X.minv32(m)))) == C.shift(32n, one) : Nat}:
  mok_inv_o(one, h1, bp, m, hM, 4294967295, {==}, W64S.and_r(U32.is_eq(U32.and(m, 1), 1), U32.is_eq(U32.mul(m, X.minv32(m)), 4294967295), hok))

# pow_mod through 32-bit Montgomery multiplication when mont32_ok(m)
def mpow_top(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +m: U32, +hM: {v(m) == 1n+bp : Nat}, +hok: {X.mont32_ok(m) == True{} : Bool}, +b: U32, +e: U32) -> {v(X.mpow32(U32.mod(b, m), e, m)) == M.pow_mod_go(140n, 1n+bp, v(e), Nat.mod(v(b), 1n+bp), Nat.mod(1n, 1n+bp)) : Nat}:
  +rb = U32.mod(b, m)
  +erb = Equal.trans(Nat, v(rb), Nat.mod(v(b), v(m)), Nat.mod(v(b), 1n+bp), UD.mod_nat(b, m, hdz(bp, m, hM)), Equal.cong(Nat, Nat, z => Nat.mod(v(b), z), v(m), 1n+bp, hM))
  +hb = L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(v(b), 1n+bp), v(rb), Equal.sym(Nat, v(rb), Nat.mod(v(b), 1n+bp), erb), mlt(bp, v(b)))
  +ev = mpow_v(one, h1, bp, m, X.minv32(m), hM, mok_inv(one, h1, bp, m, hM, hok), rb, hb, e, mok_odd(bp, m, hM, hok))
  Equal.trans(Nat, v(X.mpow32(rb, e, m)), M.pow_mod_go(140n, 1n+bp, v(e), v(rb), Nat.mod(1n, 1n+bp)), M.pow_mod_go(140n, 1n+bp, v(e), Nat.mod(v(b), 1n+bp), Nat.mod(1n, 1n+bp)), ev, Equal.cong(Nat, Nat, z => M.pow_mod_go(140n, 1n+bp, v(e), z, Nat.mod(1n, 1n+bp)), v(rb), Nat.mod(v(b), 1n+bp), erb))