law w_shr

lawful-arrays@0.1.0.0 · proof_words.bend:11

import Base

11law w_shr:
12  for +a: U32
13  {U32.to_nat(U32.shr(a)) == Nat.div(U32.to_nat(a), 2n) : Nat}