- 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

2 files changed, 73 insertions, 9 deletions

diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 0dccf64aa3..f46f6f021d 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -686,7 +686,7 @@ rewrite Qmult_div_r; try assumption.
 auto with *.
 Qed.
 
-Lemma Qle_shift_recip_l : forall a c, 
+Lemma Qle_shift_inv_l : forall a c, 
  0 < c -> a*c <= 1 -> a <= /c.
 Proof.
 intros a c Hc H.
@@ -706,7 +706,7 @@ rewrite Qmult_div_r; try assumption.
 auto with *.
 Qed.
 
-Lemma Qle_shift_recip_r : forall b c, 
+Lemma Qle_shift_inv_r : forall b c, 
  0 < b -> 1 <= c*b -> /b <= c.
 Proof.
 intros b c Hc H.
@@ -715,6 +715,57 @@ change (1/b <= c).
 apply Qle_shift_div_r; assumption.
 Qed.
 
+Lemma Qinv_lt_0_compat : forall a, 0 < a -> 0 < /a.
+Proof.
+intros [[|n|n] d] Ha; assumption.
+Qed.
+
+Lemma Qlt_shift_div_l : forall a b c,
+ 0 < c -> a*c < b -> a < b/c.
+Proof.
+intros a b c Hc H.
+apply Qnot_le_lt.
+intros H0.
+apply (Qlt_not_le _ _ H).
+apply Qmult_lt_0_le_reg_r with (/c).
+ apply Qinv_lt_0_compat.
+ assumption.
+setoid_replace (a*c/c) with (a) by (apply Qdiv_mult_l; auto with *).
+assumption.
+Qed.
+
+Lemma Qlt_shift_inv_l : forall a c,
+ 0 < c -> a*c < 1 -> a < /c.
+Proof.
+intros a c Hc H.
+setoid_replace (/c) with (1*/c) by (symmetry; apply Qmult_1_l).
+change (a < 1/c).
+apply Qlt_shift_div_l; assumption.
+Qed.
+
+Lemma Qlt_shift_div_r : forall a b c,
+ 0 < b -> a < c*b -> a/b < c.
+Proof.
+intros a b c Hc H.
+apply Qnot_le_lt.
+intros H0.
+apply (Qlt_not_le _ _ H).
+apply Qmult_lt_0_le_reg_r with (/b).
+ apply Qinv_lt_0_compat.
+ assumption.
+setoid_replace (c*b/b) with (c) by (apply Qdiv_mult_l; auto with *).
+assumption.
+Qed.
+
+Lemma Qlt_shift_inv_r : forall b c,
+ 0 < b -> 1 < c*b -> /b < c.
+Proof.
+intros b c Hc H.
+setoid_replace (/b) with (1*/b) by (symmetry; apply Qmult_1_l).
+change (1/b < c).
+apply Qlt_shift_div_r; assumption.
+Qed.
+
 (** * Rational to the n-th power *)
 
 Definition Qpower_positive (q:Q)(p:positive) : Q := 
@@ -743,4 +794,4 @@ Add Morphism Qpower with signature Qeq ==> eq ==> Qeq as Qpower_comp.
 Proof.
 intros x1 x2 Hx [|y|y]; try reflexivity;
 simpl; rewrite Hx; reflexivity.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v
index 511463ee71..b3f5e7af48 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.