law wshr

lawful-words@0.1.0.0 · proof_word.bend:662

import Base

662law wshr:
663  for +n: Nat
664  for +w: Word(n)
665  {Word.to_nat(n, Word.shr(n, w)) == Nat.div(Word.to_nat(n, w), 2n) : Nat}