Add lemmas about testbit on bounded integers

These proofs are originally by @paulzhu, which is why I put him as the author of this commit. This is a part of !244 (closed).