law lt_sub1

lawful-bytes@0.1.1.0 · proof_fast_find.bend:888

import Base

888law lt_sub1:
889  for +f: Nat
890  for +tt: Nat
891  for +h: {Nat.is_lt(f, tt) == True{} : Bool}
892  {Nat.is_le(f, Nat.sub(tt, 1n)) == True{} : Bool}