diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 11:00:20 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 11:00:20 +0100 |
| commit | 16f93d201cf7e379d5acf533be20fed30bbc212c (patch) | |
| tree | a4d1e8ee095c3892f98e80860010f118ab9e8558 /theories/QArith/Qabs.v | |
| parent | a4f37da927bc267de505da12f5e5d626af219f90 (diff) | |
| parent | f4e46fdf6072727cbfdef42a6db77d5be05d027a (diff) | |
Merge PR #6155: 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 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. |