law sub1_lt

lawful-bytes@0.1.1.0 · proof_fast_find.bend:913

import Base

913law sub1_lt:
914  for +tt: Nat
915  for +h: {Nat.is_lt(0n, tt) == True{} : Bool}
916  {Nat.is_lt(Nat.sub(tt, 1n), tt) == True{} : Bool}