def lt_pow2

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

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

96# 2^h is strictly above h - 1, i.e. n < 2^(n+1).
97def lt_pow2(+n: Nat) -> {Nat.is_lt(n,SC.pow2(n)) == True{} : Bool}:
98  match n:
99    case 0n: {==}
100    case 1n+q:
101      N.lt_le_trans(1n+q,1n+SC.pow2(q),Nat.double(SC.pow2(q)),lt_pow2(q),N.double_succ_le(SC.pow2(q),N.pow2_pos(q)))