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/Ints/num/GenSqrt.v | 14 ++------------ theories/ZArith/Zdiv.v | 17 +++++++++++++++++ 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. -- cgit v1.2.3