law wshl_mod

lawful-words@0.1.0.0 · proof_word.bend:623

import Base

623law wshl_mod:
624  for +n: Nat
625  for +w: Word(n)
626  {Word.to_nat(n, Word.shl(n, w)) == Nat.mod(Nat.double(Word.to_nat(n, w)), Nat.pow(2n, n)) : Nat}