diff options
Diffstat (limited to 'theories/QArith/Qabs.v')
| -rw-r--r-- | theories/QArith/Qabs.v | 25 |
1 files changed, 17 insertions, 8 deletions
diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v index c60d0451..31eb41bc 100644 --- a/theories/QArith/Qabs.v +++ b/theories/QArith/Qabs.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 Export QArith. @@ -26,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. @@ -86,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. @@ -100,6 +102,13 @@ rewrite Z.abs_mul. reflexivity. Qed. +Lemma Qabs_Qinv : forall q, Qabs (/ q) == / (Qabs q). +Proof. + intros [n d]; simpl. + unfold Qinv. + case_eq n; intros; simpl in *; apply Qeq_refl. +Qed. + Lemma Qabs_Qminus x y: Qabs (x - y) = Qabs (y - x). Proof. unfold Qminus, Qopp. simpl. |