Definition bitOf (n position : Z) : bit :=
  match Z.testbit n position with
  | true  => B1
  | false => B0
  end.
