def am_small

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix32.bend:193

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

193def am_small(+s: U32, +h: {Nat.is_lt(vs(s), 32n) == True{} : Bool}) -> {U32.to_nat(U32.and(s, 31)) == vs(s) : Nat}:
194  Equal.trans(Nat, U32.to_nat(U32.and(s, 31)), Nat.mod(vs(s), 32n), vs(s), am(s), R.mod_of(0n, 31n, vs(s), h))