Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements

 Mostly results about Zgcd (commutativity, associativity, ...).
 Slight improvement of ZMicromega.

 Beware: some lemmas of Zdiv/ Znumtheory were asking for
 too strict or useless hypothesis. Some minor glitches may occur.

 By the way, some iff lemmas about negb in Bool.v

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

1 files changed, 15 insertions, 22 deletions

diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 4de7e8218..f341b193e 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -588,39 +588,32 @@ Qed.
 
 (** Some additionnal inequalities about Zdiv. *)
 
-Theorem Zdiv_le_upper_bound: 
-  forall a b q, 0 <= a -> 0 < b -> a <= q*b -> a/b <= q.
+Theorem Zdiv_lt_upper_bound:
+  forall a b q, 0 < b -> a < q*b -> a/b < q.
 Proof.
-  intros a b q H1 H2 H3.
-  apply Zmult_le_reg_r with b; auto with zarith.
-  apply Zle_trans with (2 := H3).
+  intros a b q H1 H2.
+  apply Zmult_lt_reg_r with b; auto with zarith.
+  apply Zle_lt_trans with (2 := H2).
   pattern a at 2; rewrite (Z_div_mod_eq a b); auto with zarith.
   rewrite (Zmult_comm b); case (Z_mod_lt a b); auto with zarith.
 Qed.
 
-Theorem Zdiv_lt_upper_bound: 
-  forall a b q, 0 <= a -> 0 < b -> a < q*b -> a/b < q.
+Theorem Zdiv_le_upper_bound:
+  forall a b q, 0 < b -> a <= q*b -> a/b <= q.
 Proof.
-  intros a b q H1 H2 H3.
-  apply Zmult_lt_reg_r with b; auto with zarith.
-  apply Zle_lt_trans with (2 := H3).
-  pattern a at 2; rewrite (Z_div_mod_eq a b); auto with zarith.
-  rewrite (Zmult_comm b); case (Z_mod_lt a b); auto with zarith.
+  intros.
+  rewrite <- (Z_div_mult_full q b); auto with zarith.
+  apply Z_div_le; auto with zarith.
 Qed.
 
-Theorem Zdiv_le_lower_bound: 
-  forall a b q, 0 <= a -> 0 < b -> q*b <= a -> q <= a/b.
+Theorem Zdiv_le_lower_bound:
+  forall a b q, 0 < b -> q*b <= a -> q <= a/b.
 Proof.
-  intros a b q H1 H2 H3.
-  assert (q < a / b + 1); auto with zarith.
-  apply Zmult_lt_reg_r with b; auto with zarith.
-  apply Zle_lt_trans with (1 := H3).
-  pattern a at 1; rewrite (Z_div_mod_eq a b); auto with zarith.
-  rewrite Zmult_plus_distr_l; rewrite (Zmult_comm b); case (Z_mod_lt a b);
-   auto with zarith.
+  intros.
+  rewrite <- (Z_div_mult_full q b); auto with zarith.
+  apply Z_div_le; 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 ->