law lt_succ_self

lawful-words@0.1.0.0 · proof_bytes.bend:65

import Base

65law lt_succ_self:
66  for +j: Nat
67  {Nat.is_lt(j, 1n+j) == True{} : Bool}