Definition isLsbSet {n:nat} (v: Bvector n): bool.
  Proof.
    refine (
      match n as m return m <= n -> bool with
      | O => fun _ => false (* There is no LSB *)
      | S n' => fun pf => nth_order v (_:n'<n)
    end _); trivial.
    Show Proof.
  Defined.