law lt_add_l

lawful-bytes@0.1.1.0 · proof_fast_find.bend:820

import Base

820law lt_add_l:
821  for +c: Nat
822  for +a: Nat
823  for +b: Nat
824  for +h: {Nat.is_lt(a, b) == True{} : Bool}
825  {Nat.is_lt(Nat.add(c, a), Nat.add(c, b)) == True{} : Bool}