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/Qabs.v | |
| parent | 8d176db01baf9fb4a5e07decb9500ef4a8717e93 (diff) | |
Get rid of ' notation for Zpos in QArith.
Diffstat (limited to 'theories/QArith/Qabs.v')
| -rw-r--r-- | theories/QArith/Qabs.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v index ec2ac7832..ebfd78061 100644 --- a/theories/QArith/Qabs.v +++ b/theories/QArith/Qabs.v @@ -26,8 +26,8 @@ intros [xn xd] [yn yd] H. simpl. unfold Qeq in *. simpl in *. -change (' yd)%Z with (Z.abs (' yd)). -change (' xd)%Z with (Z.abs (' xd)). +change (Zpos yd)%Z with (Z.abs (Zpos yd)). +change (Zpos xd)%Z with (Z.abs (Zpos xd)). repeat rewrite <- Z.abs_mul. congruence. Qed. @@ -86,8 +86,8 @@ unfold Qplus. unfold Qle. simpl. apply Z.mul_le_mono_nonneg_r;auto with *. -change (' yd)%Z with (Z.abs (' yd)). -change (' xd)%Z with (Z.abs (' xd)). +change (Zpos yd)%Z with (Z.abs (Zpos yd)). +change (Zpos xd)%Z with (Z.abs (Zpos xd)). repeat rewrite <- Z.abs_mul. apply Z.abs_triangle. Qed. |