law lift

lawful-fields@0.1.1.0 · proof_num.bend:23

import Base

23# A bound below M gives the bound below 2^32 that lawful-words' lemmas want.
24law lift:
25  for +x: Nat
26  for +M: Nat
27  for +hm: {Nat.pow(2n, 32n) == M : Nat}
28  for +h: {Nat.is_lt(x, M) == True{} : Bool}
29  {Nat.is_lt(x, Nat.pow(2n, 32n)) == True{} : Bool}