Adding Zdiv_le_compat_l

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

1 files changed, 2 insertions, 12 deletions

diff --git a/theories/Ints/num/GenSqrt.v b/theories/Ints/num/GenSqrt.v
index 3a5b59b6dc..d1ed6353df 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]]).