feat: BitVec.ushiftRight in terms of extractLsb' (leanprover#6745)

This PR supports rewriting `ushiftRight` in terms of `extractLsb'`. This
is the companion PR to leanprover#6743 which adds the similar lemmas about
`shiftLeft`.


```lean
theorem ushiftRight_eq_zero {x : BitVec w} {n : Nat} (hn : w ≤ n) :
    x >>> n = 0#w

theorem ushiftRight_eq_extractLsb'_of_lt {x : BitVec w} {n : Nat} (hn : n < w) :
    x >>> n = ((0#n) ++ (x.extractLsb' n (w - n))).cast (by omega)
```

Author: bollu

src/Init/Data/BitVec/Lemmas.lean

@@ -1941,6 +1941,15 @@ theorem msb_shiftLeft {x : BitVec w} {n : Nat} :
     (x <<< n).msb = x.getMsbD n := by
   simp [BitVec.msb]
 
+theorem ushiftRight_eq_extractLsb'_of_lt {x : BitVec w} {n : Nat} (hn : n < w) :
+    x >>> n = ((0#n) ++ (x.extractLsb' n (w - n))).cast (by omega) := by
+  ext i hi
+  simp only [getLsbD_ushiftRight, getLsbD_cast, getLsbD_append, getLsbD_extractLsb', getLsbD_zero,
+    Bool.if_false_right, Bool.and_self_left, Bool.iff_and_self, decide_eq_true_eq]
+  intros h
+  have := lt_of_getLsbD h
+  omega
+
 /-! ### rev -/
 
 theorem getLsbD_rev (x : BitVec w) (i : Fin w) :