diff options
author | Robbert Krebbers <mail@robbertkrebbers.nl> | 2017-11-14 22:48:54 +0100 |
---|---|---|
committer | Robbert Krebbers <mail@robbertkrebbers.nl> | 2017-11-14 22:50:08 +0100 |
commit | edc5d8f0c6128949521fa331e55cc67084951bfb (patch) | |
tree | 41634b99869dc7f68137755223e462beff4824bb /theories/QArith/Qround.v | |
parent | 8d176db01baf9fb4a5e07decb9500ef4a8717e93 (diff) |
Get rid of ' notation for Zpos in QArith.
Diffstat (limited to 'theories/QArith/Qround.v')
-rw-r--r-- | theories/QArith/Qround.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v index 6e72dd2c2..a38bd21a2 100644 --- a/theories/QArith/Qround.v +++ b/theories/QArith/Qround.v @@ -78,11 +78,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 +105,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. |