Add lemmas about testbit on bounded integers
All threads resolved!
All threads resolved!
Compare changes
+ 42
− 0
@@ -486,6 +486,48 @@ Lemma Zmod_in_range q a c :
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).