law lt_add_self

lawful-words@0.1.0.0 · proof_nat.bend:801

import Base

801# b + x is never below b.
802law lt_add_self:
803  for +b: Nat
804  for +x: Nat
805  {Nat.is_lt(Nat.add(b, x), b) == False{} : Bool}