law lt_add_cancel_l

lawful-words@0.1.0.0 · proof_u32.bend:687

import Base

687law lt_add_cancel_l:
688  for +c: Nat
689  for +a: Nat
690  for +b: Nat
691  for +h: {Nat.is_lt(Nat.add(c, a), Nat.add(c, b)) == True{} : Bool}
692  {Nat.is_lt(a, b) == True{} : Bool}