Word.v: add a [wbit] function to produce a word with a single set bit
Word.v: add a [wbit] function to produce a word with a single set bit

hopefully will be useful in packing multiple bits into a word for
the bitmap allocator.

also prove some theorems about this wbit function:

  Theorem wbit_or_same : forall sz n, (n < sz)%nat
    -> (wbit sz n) ^| (wbit sz n) <> wzero sz.

  Theorem wbit_or_other : forall sz n1 n2, (n1 < sz)%nat
    -> (n2 < sz)%nat
    -> (n1 <> n2)
    -> (wbit sz n1) ^& (wbit sz n2) = wzero sz.

mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl