law last_lt

lawful-bytes@0.1.1.0 · proof_fast_find.bend:853

import Base

853# The last word holds byte to - 1: 4E < to <= 4E + 4 for E = (to - 1) / 4.
854law last_lt:
855  for +tt: Nat
856  for +h: {Nat.is_lt(0n, tt) == True{} : Bool}
857  {Nat.is_lt(Nat.mul(Nat.div(Nat.sub(tt, 1n), 4n), 4n), tt) == True{} : Bool}