law and3_lt

lawful-bytes@0.1.1.0 · proof_fast_append.bend:472

import Base

472law and3_lt:
473  for +q: U32
474  {Nat.is_lt(U32.to_nat((q .&. 3 : U32)), 4n) == True{} : Bool}