def pmo_lt

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:409

import Base
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 NR

409def pmo_lt(+mp: Nat, +d: Nat, +base: Nat, +acc: Nat, +ha: {Nat.is_lt(acc, 1n+mp) == True{} : Bool}) -> {Nat.is_lt(M.pow_mod_odd(1n+mp, d, base, acc), 1n+mp) == True{} : Bool}:
410  match d:
411    case 0n:
412      ha
413    case 1n+z:
414      NR.dm_lt(mp, Nat.mul(acc, base))