law shq

lawful-bytes@0.1.1.0 · proof_fast_append.bend:511

import Base

511# The shift of append.w is 8 * (q & 3).
512law shq:
513  for +q: U32
514  {U32.to_nat(((q .&. 3 : U32) << 3n : U32)) == Nat.mul(8n, U32.to_nat((q .&. 3 : U32))) : Nat}