def peel32

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/kdf/okm.bend:83

import Base

83def peel32(+q: Nat) -> {Nat.divmod.go(Nat.add(32n+q, 31n), 31n, 0n, 0n) == Nat.divmod.go(Nat.add(q, 31n), 31n, 1n, 0n) : Nat & Nat}:
84  {==}