law lt_add_succ

lawful-bytes@0.1.1.0 · proof_find.bend:81

import Base

81law lt_add_succ:
82  for +a: Nat
83  for +k: Nat
84  {Nat.is_lt(a, Nat.add(a, 1n+k)) == True{} : Bool}