diff options
Diffstat (limited to 'theories/QArith/Qround.v')
| -rw-r--r-- | theories/QArith/Qround.v | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v index 0ed6d557..7c5ddbb6 100644 --- a/theories/QArith/Qround.v +++ b/theories/QArith/Qround.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Import QArith. @@ -78,11 +80,11 @@ unfold Qlt. simpl. replace (n*1)%Z with n by ring. ring_simplify. -replace (n / ' d * ' d + ' d)%Z with - (('d * (n / 'd) + n mod 'd) + 'd - n mod 'd)%Z by ring. +replace (n / Zpos d * Zpos d + Zpos d)%Z with + ((Zpos d * (n / Zpos d) + n mod Zpos d) + Zpos d - n mod Zpos d)%Z by ring. rewrite <- Z_div_mod_eq; auto with*. rewrite <- Z.lt_add_lt_sub_r. -destruct (Z_mod_lt n ('d)); auto with *. +destruct (Z_mod_lt n (Zpos d)); auto with *. Qed. Hint Resolve Qlt_floor : qarith. @@ -105,9 +107,9 @@ Proof. intros [xn xd] [yn yd] Hxy. unfold Qle in *. simpl in *. -rewrite <- (Zdiv_mult_cancel_r xn ('xd) ('yd)); auto with *. -rewrite <- (Zdiv_mult_cancel_r yn ('yd) ('xd)); auto with *. -rewrite (Z.mul_comm ('yd) ('xd)). +rewrite <- (Zdiv_mult_cancel_r xn (Zpos xd) (Zpos yd)); auto with *. +rewrite <- (Zdiv_mult_cancel_r yn (Zpos yd) (Zpos xd)); auto with *. +rewrite (Z.mul_comm (Zpos yd) (Zpos xd)). apply Z_div_le; auto with *. Qed. @@ -141,7 +143,7 @@ Qed. Lemma Zdiv_Qdiv (n m: Z): (n / m)%Z = Qfloor (n / m). Proof. unfold Qfloor. intros. simpl. - destruct m as [?|?|p]; simpl. + destruct m as [ | | p]; simpl. now rewrite Zdiv_0_r, Z.mul_0_r. now rewrite Z.mul_1_r. rewrite <- Z.opp_eq_mul_m1. |