law le_cancel

lawful-bytes@0.1.1.0 · proof_fast_find.bend:294

import Base

294law le_cancel:
295  for +a: Nat
296  for +x: Nat
297  for +y: Nat
298  for +h: {Nat.is_le(Nat.add(a, x), Nat.add(a, y)) == True{} : Bool}
299  {Nat.is_le(x, y) == True{} : Bool}