law lt_sub

lawful-words@0.1.0.0 · proof_bytes.bend:486

import Base

486law lt_sub:
487  for +j: Nat
488  for +r: Nat
489  for +n: Nat
490  for +h: {Nat.is_lt(Nat.add(j, r), n) == True{} : Bool}
491  {Nat.is_lt(j, Nat.sub(n, r)) == True{} : Bool}