law sub0_nlt

lawful-fields@0.1.1.0 · proof_num.bend:540

import Base

540law sub0_nlt:
541  for +a: Nat
542  for +b: Nat
543  for +h: {Nat.sub(b, a) == 0n : Nat}
544  {Nat.is_lt(a, b) == False{} : Bool}