def pow2_lt_succ

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:447

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

447def pow2_lt_succ(+k: Nat) -> {Nat.is_lt(SC.pow2(k), SC.pow2(1n+k)) == True{} : Bool}:
448  succ_le_lt(SC.pow2(k), Nat.double(SC.pow2(k)), double_succ_le(SC.pow2(k), pow2_pos(k)))