law wdiv2

lawful-words@0.1.0.0 · proof_word.bend:651

import Base

651law wdiv2:
652  for +p: Nat
653  for +b: Bool
654  for +t: Word(p)
655  {Nat.div(Word.to_nat(1n+p, WCon{b, t}), 2n) == Word.to_nat(p, t) : Nat}