def am_small

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix64.bend:169

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

169def am_small(+s: U32, +h: {Nat.is_lt(vs(s), 64n) == True{} : Bool}) -> {U32.to_nat(U32.and(s, 63)) == vs(s) : Nat}:
170  Equal.trans(Nat, U32.to_nat(U32.and(s, 63)), Nat.mod(vs(s), 64n), vs(s), am(s), R.mod_of(0n, 63n, vs(s), h))