`bv_decide`: support for shifting by a natural number

The following example is not currently supported by bv_decide

import Std.Tactic.BVDecide

theorem ushiftRight_symbolic_shift (x : BitVec 64) (n : Nat) (h : n < 64) :
  x >>> n = (BitVec.extractLsb 63 n x).zeroExtend 64 := by
  bv_decide

It produces the error message.

error: None of the hypotheses are in the supported BitVec fragment.
There are two potential fixes for this:
1. If you are using custom BitVec constructs simplify them to built-in ones.
2. If your problem is using only built-in ones it might currently be out of reach.
   Consider expressing it in terms of different operations that are better supported.