Nat.pow2_pos: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as Nat
Lines 440-445 of bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&start_line=440&end_line=445

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

def pow2_pos(+k: Nat) -> {Nat.is_le(1n, SC.pow2(k)) == True{} : Bool}:
  match k:
    case 0n:
      {==}
    case 1n+p:
      le_trans(1n, SC.pow2(p), Nat.double(SC.pow2(p)), pow2_pos(p), double_self_le(SC.pow2(p)))

Uses (7):
  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_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=double_self_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=pow2