diff options
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 48be89417..31eb41bc9 100644 --- a/theories/QArith/Qabs.v +++ b/theories/QArith/Qabs.v @@ -28,8 +28,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. @@ -88,8 +88,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. |