diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZBits.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZBits.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v index bf03cf0205..39e9f02c53 100644 --- a/theories/Numbers/Integer/Abstract/ZBits.v +++ b/theories/Numbers/Integer/Abstract/ZBits.v @@ -710,11 +710,13 @@ Proof. intros. now rewrite <- 2 shiftl_opp_r, shiftl_shiftl, opp_sub_distr, add_comm. Qed. -Lemma shiftr_shiftr : forall a n m, 0<=n -> 0<=m -> +Lemma shiftr_shiftr : forall a n m, 0<=m -> (a >> n) >> m == a >> (n+m). Proof. - intros a n m Hn Hm. - now rewrite !shiftr_div_pow2, pow_add_r, div_div by order_pos. + intros a n p Hn. bitwise. + rewrite 3 shiftr_spec; trivial. + now rewrite (add_comm n p), add_assoc. + now apply add_nonneg_nonneg. Qed. (** shifts and constants *) |