From 97a0854fa40d727caa0350cb1f60797b16263599 Mon Sep 17 00:00:00 2001 From: thery Date: Tue, 22 Jan 2008 12:03:29 +0000 Subject: Adding Zdiv_le_compat_l git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10461 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/ZArith/Zdiv.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'theories/ZArith') 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. -- cgit v1.2.3