law lt_cancel

lawful-bytes@0.1.1.0 · proof_fast_find.bend:308

import Base

308law lt_cancel:
309  for +a: Nat
310  for +x: Nat
311  for +y: Nat
312  for +h: {Nat.is_lt(Nat.add(a, x), Nat.add(a, y)) == True{} : Bool}
313  {Nat.is_lt(x, y) == True{} : Bool}