def mod_small

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixgen.bend:111

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

111# a value below 2^k is its own low part mod 2^k
112def mod_small(+k: Nat, +n: Nat, +pp: Nat, +hp: {C.pow2(k) == 1n+pp : Nat}, +h: {Nat.is_lt(n, 1n+pp) == True{} : Bool}) -> {Nat.mod(n, 1n+pp) == n : Nat}:
113  R.mod_of(0n, pp, n, h)