law subs_lt

lawful-fields@0.1.1.0 · proof_num.bend:557

import Base

557law subs_lt:
558  for +a: Nat
559  for +b: Nat
560  for +k: Nat
561  for +h: {Nat.sub(b, a) == 1n+k : Nat}
562  {Nat.is_lt(a, b) == True{} : Bool}