law dbound_fits

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/step.bend:72

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C

72law dbound_fits:
73  for +one: Nat
74  for +h1: {one == 1n : Nat}
75  {C.fits(32n, dbound(one)) == True{} : Bool}