diff options
Diffstat (limited to 'src/Testbit.v')
| -rw-r--r-- | src/Testbit.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/Testbit.v b/src/Testbit.v index 2bfcc3df6..545c3cbce 100644 --- a/src/Testbit.v +++ b/src/Testbit.v @@ -179,9 +179,10 @@ Proof. - rewrite nth_default_cons_S. erewrite IHus; eauto using no_overflow_tail. remember (i * limb_width)%nat as k. - rewrite Z_shiftr_add_land by omega. - replace (limb_width + k - limb_width)%nat with k by omega. - reflexivity. + rewrite Z_shiftr_add_shiftl_high; rewrite ?Nat2Z.inj_add; + repeat f_equal; try omega. + rewrite Z.land_ones by apply Nat2Z.is_nonneg. + apply Z.mod_pos_bound. zero_bounds. Qed. Lemma unfold_bits_testbit : forall limb_width us n, (0 < limb_width)%nat -> |