WordPowerOfTwo.positive_power: law of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/word_power_of_two.bend as WordPowerOfTwo
Lines 185-189 of stelliferous@0.0.2.0/proofs/word_power_of_two.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/word_power_of_two.bend&start_line=185&end_line=189

import Base

law positive_power:
  for +width: Nat
  for +depth: Nat
  for fits: {Nat.is_lt(depth,width) == True{} : Bool}
  {Word.cmp(width,Word.zero(width),power(width,depth)) == LT{} : Cmp}

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.cmp.fin
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.zero
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_encoding.bend&name=false_true
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_power_of_two.bend&name=compare_zero
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_power_of_two.bend&name=power