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

added 8 commits

• 7355b65f...77cb2b8a - 7 commits from branch master
• d703fd05 - Add lemmas about testbit on bounded integers

Compare with previous version

added 1 commit

• 1d9b9a3c - Apply 2 suggestion(s) to 1 file(s)

Compare with previous version

added 1 commit

• 1ac62229 - Add lemmas about testbit on bounded integers

Compare with previous version

resolved all threads

added 1 commit

• 570b2789 - Add lemmas about testbit on bounded integers

Compare with previous version

I've added a derived lemma Z_bounded_iff_bits_nonneg' that I found useful when developing the bitvector library.

added 1 commit

• c67d6a8f - Add lemmas about testbit on bounded integers

Compare with previous version

resolved all threads

merged

mentioned in commit 6412fbd8

Thanks. LGTM.