law last_le

lawful-bytes@0.1.1.0 · proof_fast_find.bend:870

import Base

870law last_le:
871  for +tt: Nat
872  for +h: {Nat.is_lt(0n, tt) == True{} : Bool}
873  {Nat.is_le(tt, Nat.mul(Nat.add(Nat.div(Nat.sub(tt, 1n), 4n), 1n), 4n)) == True{} : Bool}