~/jendhub

def lt_pow2_succ

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake3/lists.bend:103

import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/lists.bend as Lists
import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC

103def lt_pow2_succ(+n: Nat) -> {Nat.is_lt(n,SC.pow2(1n+n)) == True{} : Bool}:
104  N.lt_trans(n,SC.pow2(n),SC.pow2(1n+n),lt_pow2(n),N.pow2_lt_succ(n))

Uses (7)

Used by (1)