law lt_dbl_bit

lawful-words@0.1.0.0 · proof_word.bend:49

import Base
import lawful-words@0.1.0.0/proof_nat.bend as N

49# b + 2x < 2y when x < y.
50law lt_dbl_bit:
51  for +x: Nat
52  for +y: Nat
53  for +b: Bool
54  for +h: {Nat.is_lt(x, y) == True{} : Bool}
55  {Nat.is_lt(Nat.add(N.bn(b), Nat.double(x)), Nat.double(y)) == True{} : Bool}