law lt_dbl_inv

lawful-words@0.1.0.0 · proof_word.bend:75

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

75# b + 2x < 2y gives x < y.
76law lt_dbl_inv:
77  for +x: Nat
78  for +y: Nat
79  for +b: Bool
80  for +h: {Nat.is_lt(Nat.add(N.bn(b), Nat.double(x)), Nat.double(y)) == True{} : Bool}
81  {Nat.is_lt(x, y) == True{} : Bool}