diff options
Diffstat (limited to 'theories/Ints/num/GenDiv.v')
| -rw-r--r-- | theories/Ints/num/GenDiv.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Ints/num/GenDiv.v b/theories/Ints/num/GenDiv.v index 3bf0615c2b..6466c198ff 100644 --- a/theories/Ints/num/GenDiv.v +++ b/theories/Ints/num/GenDiv.v @@ -944,8 +944,8 @@ Section GenDivGt. (spec_add_mul_div bh bl Hb) (spec_add_mul_div bl w_0 Hb); rewrite spec_w_0; repeat rewrite Zmult_0_l;repeat rewrite Zplus_0_l; - rewrite Zdiv_0;repeat rewrite Zplus_0_r. - Spec_w_to_Z ah;Spec_w_to_Z bh. 2:apply Zpower_lt_0;zarith. + rewrite Zdiv_0_l;repeat rewrite Zplus_0_r. + Spec_w_to_Z ah;Spec_w_to_Z bh. unfold base;repeat rewrite Zmod_shift_r;zarith. assert (H3:=to_Z_div_minus_p ah HHHH);assert(H4:=to_Z_div_minus_p al HHHH); assert (H5:=to_Z_div_minus_p bl HHHH). |