feat: add `Nat.[shiftLeft_or_distrib`, shiftLeft_xor_distrib`, shiftLeft_and_distrib`, `testBit_mul_two_pow`, `bitwise_mul_two_pow`, `shiftLeft_bitwise_distrib]` (#6630)

This PR adds theorems `Nat.[shiftLeft_or_distrib`,
shiftLeft_xor_distrib`, shiftLeft_and_distrib`, `testBit_mul_two_pow`,
`bitwise_mul_two_pow`, `shiftLeft_bitwise_distrib]`, to prove
`Nat.shiftLeft_or_distrib` by emulating the proof strategy of
`shiftRight_and_distrib`.

In particular, `Nat.shiftLeft_or_distrib` is necessary to simplify the
proofs in #6476.

---------

Co-authored-by: Alex Keizer <alex@keizer.dev>