law pad_nat

stelliferous@0.0.2.0 · proofs/u32_successor.bend:6

import Base

6law pad_nat:
7  for +n: Nat
8  for +w: Word(n)
9  {Word.to_nat(1n+n,Word.shr.pad(n,w)) == Word.to_nat(n,w) : Nat}