refactor: replace Bitvec with Std.BitVec (#5920)

re-adding definitions and theorems about bitvectors that mathlib has for `Bitvec` to the new `Std.BitVec` type, and getting rid of the former.

In std, the choice was made to define ult (unsigned less than) and related comparisons as `Bool`-valued, where the corresponding defs for `Bitvec` in mathlib are `Prop`-valued. Std does not have definitions for the respective greater-equal or greater-than comparisons, so we add those here, but we choose to be consistent with std and make them `Bool`-valued as well, breaking with the old API. 



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Alex Keizer <alex@keizer.dev>
Co-authored-by: Harun Khan <harun19@stanford.edu>