law cnt1

lawful-bytes@0.1.1.0 · proof_fast_append.bend:1168

import Base

1168# The word count (np + 3) >> 2 covers np bytes with less than one word left.
1169law cnt1:
1170  for +np: Nat
1171  {Nat.is_le(np, Nat.mul(Nat.div(Nat.add(np, 3n), 4n), 4n)) == True{} : Bool}