law lt_add_l

lawful-words@0.1.0.0 · proof_nat.bend:841

import Base

841# c + a < c + b from a < b (and the same for <=).
842law lt_add_l:
843  for +c: Nat
844  for +a: Nat
845  for +b: Nat
846  for h: {Nat.is_lt(a, b) == True{} : Bool}
847  {Nat.is_lt(Nat.add(c, a), Nat.add(c, b)) == True{} : Bool}