diff options
| author | Hugo Herbelin | 2019-07-27 23:28:54 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-07-27 23:28:54 +0200 |
| commit | bbec12e3bb2cd1062bd833bbb2c44adbeef33503 (patch) | |
| tree | caf4e355b97c7c1566601aa4c0c4523a7c1aa53f | |
| parent | 2e37b4b30d0779dc960db80189e51ecd69f7e45a (diff) | |
| parent | 75b81316d86b6a76d81b03aef891aeb6df9c814d (diff) | |
Merge PR #10569: [Int63] Remove redundant misnamed lemma lsr_add_distr
Reviewed-by: herbelin
Reviewed-by: maximedenes
Reviewed-by: silene
| -rw-r--r-- | theories/Numbers/Cyclic/Int63/Int63.v | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index 9bb16b97e2..c81ba02230 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -812,14 +812,6 @@ Proof. eapply Z.lt_le_trans; [ | apply Zpower2_le_lin ]; auto with zarith. Qed. -Lemma lsr_add_distr x y n: (x + y) << n = ((x << n) + (y << n))%int63. -Proof. - apply to_Z_inj. - rewrite -> add_spec, !lsl_spec, add_spec. - rewrite -> Zmult_mod_idemp_l, <-Zplus_mod. - apply f_equal2 with (f := Zmod); auto with zarith. -Qed. - (* LSL *) Lemma lsl0 i: 0 << i = 0%int63. Proof. @@ -1119,7 +1111,7 @@ Proof. generalize (add_le_r x y); rewrite Heq, lor_le; intro Hb. generalize Heq; rewrite (bit_split x) at 1; rewrite (bit_split y )at 1; clear Heq. rewrite (fun y => add_comm y (bit x 0)), <-!add_assoc, add_comm, - <-!add_assoc, (add_comm (bit y 0)), add_assoc, <-lsr_add_distr. + <-!add_assoc, (add_comm (bit y 0)), add_assoc, <-lsl_add_distr. rewrite (bit_split (x lor y)), lor_spec. intros Heq. assert (F: (bit x 0 + bit y 0)%int63 = (bit x 0 || bit y 0)). |