law lt_add_succ

lawful-fields@0.1.1.0 · proof_digits.bend:479

import Base

479law lt_add_succ:
480  for +p: Nat
481  for +y: Nat
482  {Nat.is_lt(p, Nat.add(p, 1n+y)) == True{} : Bool}