Adding Zdiv_le_compat_l

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

2 files changed, 19 insertions, 12 deletions

diff --git a/theories/Ints/num/GenSqrt.v b/theories/Ints/num/GenSqrt.v
index 3a5b59b6d..d1ed6353d 100644
--- a/theories/Ints/num/GenSqrt.v
+++ b/theories/Ints/num/GenSqrt.v
@@ -1116,16 +1116,6 @@ intros x; case x; simpl ww_is_even.
   simpl ww_to_Z.
   assert (V4 := spec_ww_to_Z w_digits w_to_Z spec_to_Z x);auto with zarith.
   Qed. 
-
-  Lemma Zdiv_le_monotone: forall p q r, 0 <= p -> 0 < q < r ->
-    p / r <= p / q.
-  intros p q r H H1.
-  apply Zdiv_le_lower_bound; auto with zarith.
-  rewrite Zmult_comm.
-  pattern p at 2; rewrite (Z_div_mod_eq p r); auto with zarith.
-  apply Zle_trans with (r * (p / r)); auto with zarith.
-  case (Z_mod_lt p r); auto with zarith.
-  Qed.
   
   Lemma wwB_4_2: 2 * (wwB / 4) = wwB/ 2. 
   pattern wwB at 1; rewrite wwB_wBwB; rewrite Zpower_2.
@@ -1151,10 +1141,10 @@ intros x; case x; simpl ww_is_even.
   generalize (spec_ww_head0 x H2); case (ww_head0 x);  autorewrite with rm10.
   intros (H3, H4); split; auto with zarith.
   apply Zle_trans with (2 := H3).
-  apply Zdiv_le_monotone; auto with zarith.
+  apply Zdiv_le_compat_l; auto with zarith.
   intros xh xl (H3, H4); split; auto with zarith.
   apply Zle_trans with (2 := H3).
-  apply Zdiv_le_monotone; auto with zarith.
+  apply Zdiv_le_compat_l; auto with zarith.
   intros H1.
   case (spec_to_w_Z (ww_head0 x)); intros Hv1 Hv2.
   assert (Hp0: 0 < [[ww_head0 x]]).
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index e28acb4a6..85d2b06f6 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -486,6 +486,7 @@ Proof.
   auto with zarith.
 Qed.
 
+
 (** A division of a small number by a bigger one yields zero. *)
 
 Theorem Zdiv_small: forall a b, 0 <= a < b -> a/b = 0.
@@ -604,6 +605,22 @@ Proof.
    auto with zarith.
 Qed.
 
+
+(** A division of respect opposite monotonicity for the divisor *)
+
+Lemma Zdiv_le_compat_l: forall p q r, 0 <= p -> 0 < q < r ->
+    p / r <= p / q.
+Proof.
+  intros p q r H H1. 
+  apply Zdiv_le_lower_bound; auto with zarith.
+  rewrite Zmult_comm.
+  pattern p at 2; rewrite (Z_div_mod_eq p r); auto with zarith.
+  apply Zle_trans with (r * (p / r)); auto with zarith.
+  apply Zmult_le_compat_r; auto with zarith.
+  apply Zdiv_le_lower_bound; auto with zarith.
+  case (Z_mod_lt p r); auto with zarith.
+Qed.
+
 Theorem Zdiv_sgn: forall a b, 
   0 <= Zsgn (a/b) * Zsgn a * Zsgn b.
 Proof.