law lt_pos

lawful-words@0.1.0.0 · proof_nat.bend:814

import Base

814law lt_pos:
815  for +r: Nat
816  for +b: Nat
817  for h: {Nat.is_lt(r, b) == True{} : Bool}
818  {Nat.is_lt(0n, b) == True{} : Bool}