law dbound_lt

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

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

61law dbound_lt:
62  for +one: Nat
63  for +h1: {one == 1n : Nat}
64  {Nat.is_lt(dbound(one), C.shift(30n, one)) == True{} : Bool}