- renaming Qle_shift_recip_r into Qle_shift_inv_r, etc

- Adding Qlt_shift_div_l, etc
- Adding Qabs_Qmult : forall a b, Qabs (a*b) == (Qabs a)*(Qabs b).
- Adding Qle_Qabs : forall a, a <= Qabs a.
- Removing redudnent Qminus' x y := Qred (Qminus x y) from Qabs.  It is 
already defined elsewhere (in it's proper place).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10118 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 19 insertions, 6 deletions

diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v
index 511463ee7..b3f5e7af4 100644
--- a/theories/QArith/Qabs.v
+++ b/theories/QArith/Qabs.v
@@ -84,6 +84,25 @@ repeat rewrite <- Zabs_Zmult.
 apply Zabs_triangle.
 Qed.
 
+Lemma Qabs_Qmult : forall a b, Qabs (a*b) == (Qabs a)*(Qabs b).
+Proof.
+intros [an ad] [bn bd].
+simpl.
+rewrite Zabs_Zmult.
+reflexivity.
+Qed.
+
+Lemma Qle_Qabs : forall a, a <= Qabs a.
+Proof.
+intros a.
+apply Qabs_case; auto with *.
+intros H.
+apply Qle_trans with 0; try assumption.
+change 0 with (-0).
+apply Qopp_le_compat.
+assumption.
+Qed.
+
 Lemma Qabs_triangle_reverse : forall x y, Qabs x - Qabs y <= Qabs (x - y).
 Proof.
 intros x y.
@@ -95,9 +114,3 @@ apply Qabs_triangle.
 apply Qabs_wd.
 ring.
 Qed.
-
-Definition Qminus' x y := Qred (Qminus x y).
-Lemma Qminus'_correct : forall p q : Q, (Qminus' p q)==(Qminus p q).
-Proof.
-  intros; unfold Qminus' in |- *; apply Qred_correct; auto.
-Qed.