def odd_lt

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

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 R

65def odd_lt(+mp: Nat, +bit: Nat, +base: Nat, +acc: Nat, +hacc: {Nat.is_lt(acc, 1n+mp) == True{} : Bool}) -> {Nat.is_lt(M.pow_mod_odd(1n+mp, bit, base, acc), 1n+mp) == True{} : Bool}:
66  match bit:
67    case 0n:
68      hacc
69    case 1n+z:
70      R.dm_lt(mp, Nat.mul(acc, base))