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).
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).