Nat.pow2_lt_succ: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as Nat
Lines 447-448 of bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&start_line=447&end_line=448

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

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

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=double_succ_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=pow2_pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=succ_le_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=pow2