Extension of bitops/ihsext-basics with additional lemmas.
BOZO this needs a lot of documentation. For now you're best off looking at the source code.
