law power_monotone

stelliferous@0.0.2.0 · proofs/word_power_of_two.bend:217

import Base

217law power_monotone:
218  for +width: Nat
219  for +lower: Nat
220  for +upper: Nat
221  for fits: {Nat.is_lt(upper,width) == True{} : Bool}
222  for ordered: {Nat.is_le(lower,upper) == True{} : Bool}
223  {Cmp.is_le(Word.cmp(width,power(width,lower),power(width,upper))) == True{} : Bool}