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, 17 insertions, 0 deletions

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.