law positive_power

stelliferous@0.0.2.0 · proofs/word_power_of_two.bend:185

import Base

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