law tl_lt

lawful-bytes@0.1.1.0 · proof_same.bend:281

import Base

281law tl_lt:
282  for +a: Nat
283  for +b: Nat
284  for +h: {Nat.is_lt(1n+a, b) == True{} : Bool}
285  {Nat.is_lt(a, b) == True{} : Bool}