Fix bug #1899: no more strange notations for Qge and Qgt

In fact, Qge and Ggt disappear, and we only leave notations for > and >=
that map directly to Qlt and Qle. 

We also adopt the same approach for BigN, BigZ, BigQ.

By the way, various clean-up concerning Zeq_bool, Zle_bool and similar
functions for Q. 



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

13 files changed, 208 insertions, 206 deletions

diff --git a/contrib/micromega/QMicromega.v b/contrib/micromega/QMicromega.v
index 9e95f6c49..c054f218a 100644
--- a/contrib/micromega/QMicromega.v
+++ b/contrib/micromega/QMicromega.v
@@ -16,38 +16,11 @@ Require Import OrderedRing.
 Require Import RingMicromega.
 Require Import Refl.
 Require Import QArith.
-Require Import Qring.
-
-(* Qsrt has been removed from the library ? *)
-Definition Qsrt : ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq.
-Proof.
-  constructor.
-  exact Qplus_0_l.
-  exact Qplus_comm.
-  exact Qplus_assoc.
-  exact Qmult_1_l.
-  exact Qmult_comm.
-  exact Qmult_assoc.
-  exact Qmult_plus_distr_l.
-  reflexivity.
-  exact Qplus_opp_r.
-Qed.
-
-
-Add Ring Qring : Qsrt.
-
-Lemma Qmult_neutral : forall x , 0 * x == 0.
-Proof.
-  intros.
-  compute.
-  reflexivity.
-Qed.
-
-(* Is there any qarith database ? *)
+Require Import Qfield.
 
 Lemma Qsor : SOR 0 1 Qplus Qmult Qminus Qopp Qeq  Qle Qlt.
 Proof.
-  constructor; intros ; subst ; try (intuition (subst; auto  with qarith)).
+  constructor; intros ; subst ; try (intuition (subst; auto with qarith)).
   apply Q_Setoid.
   rewrite H ; rewrite H0 ; reflexivity.
   rewrite H ; rewrite H0 ; reflexivity.
@@ -67,45 +40,12 @@ Proof.
   destruct(Q_dec n m) as [[H1 |H1] | H1 ] ; tauto.
   apply (Qplus_le_compat  p p n m  (Qle_refl p) H).
   generalize (Qmult_lt_compat_r 0 n m H0 H).
-  rewrite Qmult_neutral.
+  rewrite Qmult_0_l.
   auto.
   compute in H.
   discriminate.
 Qed.
 
-Definition Qeq_bool (p q : Q) : bool := Zeq_bool (Qnum p * ' Qden q)%Z  (Qnum q * ' Qden p)%Z.
-
-Definition Qle_bool (x y : Q) : bool := Zle_bool (Qnum x * ' Qden y)%Z (Qnum y * ' Qden x)%Z.
-
-Require ZMicromega.
-
-Lemma Qeq_bool_ok : forall x y, Qeq_bool x y = true -> x == y.
-Proof.
-  intros.
-  unfold Qeq_bool in H.
-  unfold Qeq.
-  apply (Zeqb_ok  _ _ H).
-Qed.
-
-
-Lemma Qeq_bool_neq : forall x y, Qeq_bool x y = false -> ~ x == y.
-Proof.
-  unfold Qeq_bool,Qeq.
-  red ; intros ; subst.
-  rewrite H0 in H.
-  apply  (ZMicromega.Zeq_bool_neq _ _ H).
-  reflexivity.
-Qed.
-
-Lemma Qle_bool_imp_le : forall x y : Q, Qle_bool x y = true -> x <= y.
-Proof.
-  unfold Qle_bool, Qle.
-  intros.
-  apply Zle_bool_imp_le ; auto.
-Qed.
-  
-
-
 
 Lemma QSORaddon :
   SORaddon 0 1 Qplus Qmult Qminus Qopp  Qeq  Qle (* ring elements *)
@@ -115,7 +55,7 @@ Lemma QSORaddon :
 Proof.
   constructor.
   constructor ; intros ; try reflexivity.
-  apply Qeq_bool_ok ; auto.
+  apply Qeq_bool_eq; auto.
   constructor.
   reflexivity.
   intros x y.
@@ -173,9 +113,9 @@ match o with
 | OpEq =>  Qeq
 | OpNEq => fun x y  => ~ x == y
 | OpLe => Qle
-| OpGe => Qge
+| OpGe => fun x y => Qle y x
 | OpLt => Qlt
-| OpGt => Qgt
+| OpGt => fun x y => Qlt y x
 end.
 
 Definition Qeval_formula (e:PolEnv Q) (ff : Formula Q) :=
diff --git a/contrib/micromega/RMicromega.v b/contrib/micromega/RMicromega.v
index d98c6d422..7c6969c2f 100644
--- a/contrib/micromega/RMicromega.v
+++ b/contrib/micromega/RMicromega.v
@@ -76,12 +76,12 @@ Proof.
   apply mult_IZR.
   apply Ropp_Ropp_IZR.
   apply IZR_eq.
-  apply Zeqb_ok ; auto.
+  apply Zeq_bool_eq ; auto.
   apply R_power_theory.
   intros x y.
   intro.
   apply IZR_neq.
-  apply ZMicromega.Zeq_bool_neq ; auto.
+  apply Zeq_bool_neq ; auto.
   intros. apply IZR_le.  apply Zle_bool_imp_le. auto.
 Qed.
 
diff --git a/contrib/micromega/ZMicromega.v b/contrib/micromega/ZMicromega.v
index 94c83f73d..0855925a3 100644
--- a/contrib/micromega/ZMicromega.v
+++ b/contrib/micromega/ZMicromega.v
@@ -39,15 +39,6 @@ Proof.
   apply Zmult_lt_0_compat ; auto.
 Qed.
 
-Lemma Zeq_bool_neq : forall x y, Zeq_bool x y = false -> x <> y.
-Proof.
-  red ; intros.
-  subst.
-  unfold Zeq_bool in H.
-  rewrite Zcompare_refl  in H.
-  discriminate.
-Qed.
-
 Lemma ZSORaddon :
   SORaddon 0 1 Zplus Zmult Zminus Zopp  (@eq Z) Zle (* ring elements *)
   0%Z 1%Z Zplus Zmult Zminus Zopp (* coefficients *)
@@ -56,7 +47,7 @@ Lemma ZSORaddon :
 Proof.
   constructor.
   constructor ; intros ; try reflexivity.
-  apply Zeqb_ok ; auto.
+  apply Zeq_bool_eq ; auto.
   constructor.
   reflexivity.
   intros x y.
diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v
index c1fa963f2..e664b3b76 100644
--- a/contrib/setoid_ring/InitialRing.v
+++ b/contrib/setoid_ring/InitialRing.v
@@ -38,14 +38,6 @@ Proof.
  exact Zmult_plus_distr_l. trivial. exact Zminus_diag.
 Qed.
 
- Lemma Zeqb_ok : forall x y, Zeq_bool x y = true -> x = y.
- Proof.
-  intros x y.
-  assert (H := Zcompare_Eq_eq x y);unfold Zeq_bool;
-  destruct (Zcompare x y);intros H1;auto;discriminate H1.
- Qed.
-
-
 (** Two generic morphisms from Z to (abrbitrary) rings, *)
 (**second one is more convenient for proofs but they are ext. equal*)
 Section ZMORPHISM.
@@ -174,7 +166,7 @@ Section ZMORPHISM.
    Zeq_bool x y = true -> [x] == [y].
  Proof.
   intros x y H.
-  assert (H1 := Zeqb_ok x y H);unfold IDphi in H1.
+  assert (H1 := Zeq_bool_eq x y H);unfold IDphi in H1.
   rewrite H1;rrefl.
  Qed.
   
diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v
index 4a5b623b4..942915abf 100644
--- a/contrib/setoid_ring/ZArithRing.v
+++ b/contrib/setoid_ring/ZArithRing.v
@@ -50,7 +50,7 @@ Ltac Zpower_neg :=
   end.   
 
 Add Ring Zr : Zth
-  (decidable Zeqb_ok, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc],
+  (decidable Zeq_bool_eq, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc],
    power_tac Zpower_theory [Zpow_tac],
     (* The two following option are not needed, it is the default chose when the set of 
         coefficiant is usual ring Z *)
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index bb2c01437..5189a33ef 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -42,25 +42,27 @@ Infix "?=" := BigZ.compare : bigZ_scope.
 Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope.
 Infix "<" := BigZ.lt : bigZ_scope.
 Infix "<=" := BigZ.le : bigZ_scope.
+Notation "x > y" := (BigZ.lt y x)(only parsing) : bigZ_scope.
+Notation "x >= y" := (BigZ.le y x)(only parsing) : bigZ_scope.
 Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
 
 Open Scope bigZ_scope.
 
 (** Some additional results about [BigZ] *)
 
-Theorem spec_to_Z: forall n:bigZ, 
+Theorem spec_to_Z: forall n:bigZ,
   BigN.to_Z (BigZ.to_N n) = ((Zsgn [n]) * [n])%Z.
 Proof.
-intros n; case n; simpl; intros p; 
+intros n; case n; simpl; intros p;
   generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
 intros p1 H1; case H1; auto.
 intros p1 H1; case H1; auto.
 Qed.
 
-Theorem spec_to_N n: 
+Theorem spec_to_N n:
  ([n] = Zsgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z.
 Proof.
-intros n; case n; simpl; intros p; 
+intros n; case n; simpl; intros p;
   generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
 intros p1 H1; case H1; auto.
 intros p1 H1; case H1; auto.
@@ -69,7 +71,7 @@ Qed.
 Theorem spec_to_Z_pos: forall n, (0 <= [n])%Z ->
   BigN.to_Z (BigZ.to_N n) = [n].
 Proof.
-intros n; case n; simpl; intros p; 
+intros n; case n; simpl; intros p;
   generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
 intros p1 _ H1; case H1; auto.
 intros p1 H1; case H1; auto.
@@ -87,7 +89,7 @@ Qed.
 
 (** [BigZ] is a ring *)
 
-Lemma BigZring : 
+Lemma BigZring :
  ring_theory BigZ.zero BigZ.one BigZ.add BigZ.mul BigZ.sub BigZ.opp BigZ.eq.
 Proof.
 constructor.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 1e0b45cd2..653170e34 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -47,6 +47,8 @@ Infix "?=" := BigN.compare : bigN_scope.
 Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope.
 Infix "<" := BigN.lt : bigN_scope.
 Infix "<=" := BigN.le : bigN_scope.
+Notation "x > y" := (BigN.lt y x)(only parsing) : bigN_scope.
+Notation "x >= y" := (BigN.le y x)(only parsing) : bigN_scope.
 Notation "[ i ]" := (BigN.to_Z i) : bigN_scope.
 
 Open Scope bigN_scope.
@@ -62,7 +64,7 @@ Qed.
 
 (** [BigN] is a semi-ring *)
 
-Lemma BigNring : 
+Lemma BigNring :
  semi_ring_theory BigN.zero BigN.one BigN.add BigN.mul BigN.eq.
 Proof.
 constructor.
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index 11c945f4e..4177fc202 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -54,7 +54,9 @@ Infix "?=" := BigQ.compare : bigQ_scope.
 Infix "==" := BigQ.eq : bigQ_scope.
 Infix "<" := BigQ.lt : bigQ_scope.
 Infix "<=" := BigQ.le : bigQ_scope.
-Notation "[ q ]" := (BigQ.to_Q q) : bigQ_scope. 
+Notation "x > y" := (BigQ.lt y x)(only parsing) : bigQ_scope.
+Notation "x >= y" := (BigQ.le y x)(only parsing) : bigQ_scope.
+Notation "[ q ]" := (BigQ.to_Q q) : bigQ_scope.
 
 Open Scope bigQ_scope.
 
@@ -97,16 +99,16 @@ Proof.
 Qed.
 
 (* TODO : fix this. For the moment it's useless (horribly slow)
-Hint Rewrite 
+Hint Rewrite
  BigQ.spec_0 BigQ.spec_1 BigQ.spec_m1 BigQ.spec_compare
- BigQ.spec_red BigQ.spec_add BigQ.spec_sub BigQ.spec_opp 
+ BigQ.spec_red BigQ.spec_add BigQ.spec_sub BigQ.spec_opp
  BigQ.spec_mul BigQ.spec_inv BigQ.spec_div BigQ.spec_power_pos
  BigQ.spec_square : bigq. *)
 
 
 (** [BigQ] is a field *)
 
-Lemma BigQfieldth : 
+Lemma BigQfieldth :
  field_theory BigQ.zero BigQ.one BigQ.add BigQ.mul BigQ.sub BigQ.opp BigQ.div BigQ.inv BigQ.eq.
 Proof.
 constructor.
@@ -128,7 +130,7 @@ rewrite BigQ.spec_mul, BigQ.spec_inv, BigQ.spec_1; field.
 rewrite <- BigQ.spec_0; auto.
 Qed.
 
-Lemma BigQpowerth : 
+Lemma BigQpowerth :
  power_theory BigQ.one BigQ.mul BigQ.eq Z_of_N BigQ.power.
 Proof.
 constructor.
@@ -141,13 +143,13 @@ induction p; simpl; auto; try rewrite !BigQ.spec_mul, !IHp; apply Qeq_refl.
 destruct n; reflexivity.
 Qed.
 
-Lemma BigQ_eq_bool_correct : 
+Lemma BigQ_eq_bool_correct :
  forall x y, BigQ.eq_bool x y = true -> x==y.
 Proof.
 intros; generalize (BigQ.spec_eq_bool x y); rewrite H; auto.
 Qed.
 
-Lemma BigQ_eq_bool_complete : 
+Lemma BigQ_eq_bool_complete :
  forall x y, x==y -> BigQ.eq_bool x y = true.
 Proof.
 intros; generalize (BigQ.spec_eq_bool x y).
@@ -156,16 +158,16 @@ Qed.
 
 (* TODO : improve later the detection of constants ... *)
 
-Ltac BigQcst t := 
- match t with 
+Ltac BigQcst t :=
+ match t with
    | BigQ.zero => BigQ.zero
    | BigQ.one => BigQ.one
    | BigQ.minus_one => BigQ.minus_one
-   | _ => NotConstant 
+   | _ => NotConstant
  end.
 
-Add Field BigQfield : BigQfieldth 
- (decidable BigQ_eq_bool_correct, 
+Add Field BigQfield : BigQfieldth
+ (decidable BigQ_eq_bool_correct,
   completeness BigQ_eq_bool_complete,
   constants [BigQcst],
   power_tac BigQpowerth [Qpow_tac]).
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index bfed32f9d..82d65dafb 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -155,15 +155,6 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
    generalize (Z.spec_eq_bool x y); case Z.eq_bool
   end).
 
- Ltac destr_zcompare := 
- match goal with |- context [Zcompare ?x ?y] => 
-  let H := fresh "H" in 
-  case_eq (Zcompare x y); intro H;
-   [generalize (Zcompare_Eq_eq _ _ H); clear H; intro H |
-    change (x<y)%Z in H | 
-    change (x>y)%Z in H ]
- end.
-
  Ltac simpl_ndiv := rewrite N.spec_div by (nzsimpl; romega).
  Tactic Notation "simpl_ndiv" "in" "*" := 
    rewrite N.spec_div in * by (nzsimpl; romega).
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 2265715b7..9ebfa19cb 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -10,7 +10,7 @@
 
 Require Export ZArith.
 Require Export ZArithRing.
-Require Export Setoid.
+Require Export Setoid Bool.
 
 (** * Definition of [Q] and basic properties *)
 
@@ -28,7 +28,7 @@ Ltac simpl_mult := repeat rewrite Zpos_mult_morphism.
 
 Notation "a # b" := (Qmake a b) (at level 55, no associativity) : Q_scope.
 
-Definition inject_Z (x : Z) := Qmake x 1. 
+Definition inject_Z (x : Z) := Qmake x 1.
 Arguments Scope inject_Z [Z_scope].
 
 Notation " 'QDen'  p " := (Zpos (Qden p)) (at level 20, no associativity) : Q_scope.
@@ -38,14 +38,12 @@ Notation " 1 " := (1#1) : Q_scope.
 Definition Qeq (p q : Q) := (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z.
 Definition Qle (x y : Q) := (Qnum x * QDen y <= Qnum y * QDen x)%Z.
 Definition Qlt (x y : Q) := (Qnum x * QDen y < Qnum y * QDen x)%Z.
-Notation Qgt := (fun a b : Q => Qlt b a).
-Notation Qge := (fun a b : Q => Qle b a).
 
-Infix "==" := Qeq (at level 70, no associativity) : Q_scope. 
+Infix "==" := Qeq (at level 70, no associativity) : Q_scope.
 Infix "<" := Qlt : Q_scope.
-Infix ">" := Qgt : Q_scope.
 Infix "<=" := Qle : Q_scope.
-Infix ">=" := Qge : Q_scope.
+Notation "x > y" := (Qlt y x)(only parsing) : Q_scope.
+Notation "x >= y" := (Qle y x)(only parsing) : Q_scope.
 Notation "x <= y <= z" := (x<=y/\y<=z) : Q_scope.
 
 (** Another approach : using Qcompare for defining order relations. *)
@@ -84,7 +82,7 @@ rewrite Zcompare_Gt_Lt_antisym; auto.
 rewrite Zcompare_Gt_Lt_antisym in H; auto.
 Qed.
 
-Hint Unfold Qeq Qlt Qle: qarith.
+Hint Unfold Qeq Qlt Qle : qarith.
 Hint Extern 5 (?X1 <> ?X2) => intro; discriminate: qarith.
 
 (** * Properties of equality. *)
@@ -94,7 +92,7 @@ Proof.
  auto with qarith.
 Qed.
 
-Theorem Qeq_sym : forall x y, x == y -> y == x. 
+Theorem Qeq_sym : forall x y, x == y -> y == x.
 Proof.
  auto with qarith.
 Qed.
@@ -102,7 +100,7 @@ Qed.
 Theorem Qeq_trans : forall x y z, x == y -> y == z -> x == z.
 Proof.
 unfold Qeq in |- *; intros.
-apply Zmult_reg_l with (QDen y). 
+apply Zmult_reg_l with (QDen y).
 auto with qarith.
 transitivity (Qnum x * QDen y * QDen z)%Z; try ring.
 rewrite H.
@@ -117,6 +115,44 @@ Proof.
  intros; case (Z_eq_dec (Qnum x * QDen y) (Qnum y * QDen x)); auto.
 Defined.
 
+Definition Qeq_bool x y :=
+  (Zeq_bool (Qnum x * QDen y) (Qnum y * QDen x))%Z.
+
+Definition Qle_bool x y := 
+  (Zle_bool (Qnum x * QDen y) (Qnum y * QDen x))%Z.
+
+Lemma Qeq_bool_iff : forall x y, Qeq_bool x y = true <-> x == y.
+Proof.
+  unfold Qeq_bool, Qeq; intros. 
+  symmetry; apply Zeq_is_eq_bool.
+Qed.
+
+Lemma Qeq_bool_eq : forall x y, Qeq_bool x y = true -> x == y.
+Proof.
+  intros; rewrite <- Qeq_bool_iff; auto.
+Qed.
+
+Lemma Qeq_eq_bool : forall x y, x == y -> Qeq_bool x y = true.
+Proof.
+  intros; rewrite Qeq_bool_iff; auto.
+Qed.
+
+Lemma Qeq_bool_neq : forall x y, Qeq_bool x y = false -> ~ x == y.
+Proof.
+  intros x y H; rewrite <- Qeq_bool_iff, H; discriminate.
+Qed.
+
+Lemma Qle_bool_iff : forall x y, Qle_bool x y = true <-> x <= y.
+Proof.
+  unfold Qle_bool, Qle; intros.
+  symmetry; apply Zle_is_le_bool.
+Qed.
+
+Lemma Qle_bool_imp_le : forall x y, Qle_bool x y = true -> x <= y.
+Proof.
+  intros; rewrite <- Qle_bool_iff; auto.
+Qed.
+
 (** We now consider [Q] seen as a setoid. *)
 
 Definition Q_Setoid : Setoid_Theory Q Qeq.
@@ -130,7 +166,7 @@ Hint Resolve (Seq_refl Q Qeq Q_Setoid): qarith.
 Hint Resolve (Seq_sym Q Qeq Q_Setoid): qarith.
 Hint Resolve (Seq_trans Q Qeq Q_Setoid): qarith.
 
-Theorem Qnot_eq_sym : forall x y, ~x == y -> ~y == x. 
+Theorem Qnot_eq_sym : forall x y, ~x == y -> ~y == x.
 Proof.
  auto with qarith.
 Qed.
@@ -139,13 +175,13 @@ Hint Resolve Qnot_eq_sym : qarith.
 
 (** * Addition, multiplication and opposite *)
 
-(** The addition, multiplication and opposite are defined 
+(** The addition, multiplication and opposite are defined
    in the straightforward way: *)
 
 Definition Qplus (x y : Q) :=
   (Qnum x * QDen y + Qnum y * QDen x) # (Qden x * Qden y).
 
-Definition Qmult (x y : Q) := (Qnum x * Qnum y) # (Qden x * Qden y). 
+Definition Qmult (x y : Q) := (Qnum x * Qnum y) # (Qden x * Qden y).
 
 Definition Qopp (x : Q) := (- Qnum x) # (Qden x).
 
@@ -164,8 +200,8 @@ Infix "+" := Qplus : Q_scope.
 Notation "- x" := (Qopp x) : Q_scope.
 Infix "-" := Qminus : Q_scope.
 Infix "*" := Qmult : Q_scope.
-Notation "/ x" := (Qinv x) : Q_scope. 
-Infix "/" := Qdiv : Q_scope. 
+Notation "/ x" := (Qinv x) : Q_scope.
+Infix "/" := Qdiv : Q_scope.
 
 (** A light notation for [Zpos] *)
 
@@ -181,7 +217,7 @@ Qed.
 
 (** * Setoid compatibility results *)
 
-Add Morphism Qplus : Qplus_comp. 
+Add Morphism Qplus : Qplus_comp.
 Proof.
   unfold Qeq, Qplus; simpl.
   Open Scope Z_scope.
@@ -208,7 +244,7 @@ Qed.
 Add Morphism Qminus : Qminus_comp.
 Proof.
   intros.
-  unfold Qminus. 
+  unfold Qminus.
   rewrite H; rewrite H0; auto with qarith.
 Qed.
 
@@ -232,11 +268,11 @@ Proof.
   Open Scope Z_scope.
   intros (p1, p2) (q1, q2); simpl.
   case p1; simpl.
-  intros. 
+  intros.
   assert (q1 = 0).
   elim (Zmult_integral q1 ('p2)); auto with zarith.
   intros; discriminate.
-  subst; auto. 
+  subst; auto.
   case q1; simpl; intros; try discriminate.
   rewrite (Pmult_comm p2 p); rewrite (Pmult_comm q2 p0); auto.
   case q1; simpl; intros; try discriminate.
@@ -254,7 +290,7 @@ Add Morphism Qle with signature Qeq ==> Qeq ==> iff as Qle_comp.
 Proof.
   cut (forall x1 x2, x1==x2 -> forall x3 x4, x3==x4 -> x1<=x3 -> x2<=x4).
   split; apply H; assumption || (apply Qeq_sym ; assumption).
-  
+
   unfold Qeq, Qle; simpl.
   Open Scope Z_scope.
   intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0 H1; simpl in *.
@@ -289,14 +325,26 @@ Proof.
   replace (s1 * 'q2 * 'p2 * 'r2) with (s1 * 'r2 * 'q2 * 'p2) by ring.
   rewrite <- H0.
   replace (p1 * 'q2 * 's2 * 'r2) with ('q2 * 's2 * (p1 * 'r2)) by ring.
-  replace (r1 * 's2 * 'q2 * 'p2) with ('q2 * 's2 * (r1 * 'p2)) by ring. 
+  replace (r1 * 's2 * 'q2 * 'p2) with ('q2 * 's2 * (r1 * 'p2)) by ring.
   apply Zlt_gt.
   apply Zmult_gt_0_lt_compat_l; auto with zarith.
   Close Scope Z_scope.
 Qed.
 
+Add Morphism Qeq_bool with signature Qeq ==> Qeq ==> (@eq bool) as Qeqb_comp.
+Proof.
+ intros; apply eq_true_iff_eq.
+ rewrite 2 Qeq_bool_iff, H, H0; split; auto with qarith.
+Qed.
+
+Add Morphism Qle_bool with signature Qeq ==> Qeq ==> (@eq bool) as Qleb_comp.
+Proof.
+ intros; apply eq_true_iff_eq.
+ rewrite 2 Qle_bool_iff, H, H0.
+ split; auto with qarith.
+Qed.
 
-Lemma Qcompare_egal_dec: forall n m p q : Q, 
+Lemma Qcompare_egal_dec: forall n m p q : Q,
   (n<m -> p<q) -> (n==m -> p==q) -> (n>m -> p>q) -> ((n?=m) = (p?=q)).
 Proof.
   intros.
@@ -306,7 +354,6 @@ Proof.
   omega.
 Qed.
 
-
 Add Morphism Qcompare : Qcompare_comp.
 Proof.
   intros; apply Qcompare_egal_dec; rewrite H; rewrite H0; auto.
@@ -341,7 +388,7 @@ Lemma Qplus_0_r : forall x, x+0 == x.
 Proof.
   intros (x1, x2); unfold Qeq, Qplus; simpl.
   rewrite Pmult_comm; simpl; ring.
-Qed. 
+Qed.
 
 (** Commutativity of addition: *)
 
@@ -374,6 +421,18 @@ Proof.
   intros; red; simpl; rewrite Pmult_assoc; ring.
 Qed.
 
+(** multiplication and zero *)
+
+Lemma Qmult_0_l : forall x , 0*x == 0.
+Proof.
+  intros; compute; reflexivity.
+Qed.
+
+Lemma Qmult_0_r : forall x , x*0 == 0.
+Proof.
+  intros; red; simpl; ring.
+Qed.
+
 (** [1] is a neutral element for multiplication: *)
 
 Lemma Qmult_1_l : forall n, 1*n == n.
@@ -385,7 +444,7 @@ Theorem Qmult_1_r : forall n, n*1==n.
 Proof.
   intro; red; simpl.
   rewrite Zmult_1_r with (n := Qnum n).
-  rewrite Pmult_comm; simpl; trivial. 
+  rewrite Pmult_comm; simpl; trivial.
 Qed.
 
 (** Commutativity of multiplication *)
@@ -427,7 +486,7 @@ Proof.
   rewrite <- H0; ring.
 Qed.
 
-(** * Inverse and division. *) 
+(** * Inverse and division. *)
 
 Lemma Qinv_involutive : forall q, (/ / q) == q.
 Proof.
@@ -438,13 +497,13 @@ Theorem Qmult_inv_r : forall x, ~ x == 0 -> x*(/x) == 1.
 Proof.
   intros (x1, x2); unfold Qeq, Qdiv, Qmult; case x1; simpl;
     intros; simpl_mult; try ring.
-  elim H; auto. 
+  elim H; auto.
 Qed.
 
 Lemma Qinv_mult_distr : forall p q, / (p * q) == /p * /q.
 Proof.
   intros (x1,x2) (y1,y2); unfold Qeq, Qinv, Qmult; simpl.
-  destruct x1; simpl; auto; 
+  destruct x1; simpl; auto;
     destruct y1; simpl; auto.
 Qed.
 
@@ -485,10 +544,10 @@ Proof.
   red; trivial.
   apply Zle_trans with (y1 * 'x2 * 'z2).
   replace (x1 * 'z2 * 'y2) with (x1 * 'y2 * 'z2) by ring.
-  apply Zmult_le_compat_r; auto with zarith. 
+  apply Zmult_le_compat_r; auto with zarith.
   replace (y1 * 'x2 * 'z2) with (y1 * 'z2 * 'x2) by ring.
   replace (z1 * 'x2 * 'y2) with (z1 * 'y2 * 'x2) by ring.
-  apply Zmult_le_compat_r; auto with zarith. 
+  apply Zmult_le_compat_r; auto with zarith.
   Close Scope Z_scope.
 Qed.
 
@@ -516,9 +575,9 @@ Proof.
   apply Zgt_le_trans with (y1 * 'x2 * 'z2).
   replace (y1 * 'x2 * 'z2) with (y1 * 'z2 * 'x2) by ring.
   replace (z1 * 'x2 * 'y2) with (z1 * 'y2 * 'x2) by ring.
-  apply Zmult_gt_compat_r; auto with zarith. 
+  apply Zmult_gt_compat_r; auto with zarith.
   replace (x1 * 'z2 * 'y2) with (x1 * 'y2 * 'z2) by ring.
-  apply Zmult_le_compat_r; auto with zarith. 
+  apply Zmult_le_compat_r; auto with zarith.
   Close Scope Z_scope.
 Qed.
 
@@ -532,9 +591,9 @@ Proof.
   apply Zle_gt_trans with (y1 * 'x2 * 'z2).
   replace (y1 * 'x2 * 'z2) with (y1 * 'z2 * 'x2) by ring.
   replace (z1 * 'x2 * 'y2) with (z1 * 'y2 * 'x2) by ring.
-  apply Zmult_le_compat_r; auto with zarith. 
+  apply Zmult_le_compat_r; auto with zarith.
   replace (x1 * 'z2 * 'y2) with (x1 * 'y2 * 'z2) by ring.
-  apply Zmult_gt_compat_r; auto with zarith. 
+  apply Zmult_gt_compat_r; auto with zarith.
   Close Scope Z_scope.
 Qed.
 
@@ -572,7 +631,7 @@ Proof.
   unfold Qle, Qlt, Qeq; intros; apply Zle_lt_or_eq; auto.
 Qed.
 
-Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le 
+Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le
  Qlt_le_weak Qlt_not_eq Qle_antisym Qle_refl: qartih.
 
 (** Some decidability results about orders. *)
@@ -679,7 +738,7 @@ Proof.
 intros [[|n|n] d] Ha; assumption.
 Qed.
 
-Lemma Qle_shift_div_l : forall a b c, 
+Lemma Qle_shift_div_l : forall a b c,
  0 < c -> a*c <= b -> a <= b/c.
 Proof.
 intros a b c Hc H.
@@ -690,7 +749,7 @@ rewrite Qmult_div_r; try assumption.
 auto with *.
 Qed.
 
-Lemma Qle_shift_inv_l : forall a c, 
+Lemma Qle_shift_inv_l : forall a c,
  0 < c -> a*c <= 1 -> a <= /c.
 Proof.
 intros a c Hc H.
@@ -699,7 +758,7 @@ change (a <= 1/c).
 apply Qle_shift_div_l; assumption.
 Qed.
 
-Lemma Qle_shift_div_r : forall a b c, 
+Lemma Qle_shift_div_r : forall a b c,
  0 < b -> a <= c*b -> a/b <= c.
 Proof.
 intros a b c Hc H.
@@ -710,7 +769,7 @@ rewrite Qmult_div_r; try assumption.
 auto with *.
 Qed.
 
-Lemma Qle_shift_inv_r : forall b c, 
+Lemma Qle_shift_inv_r : forall b c,
  0 < b -> 1 <= c*b -> /b <= c.
 Proof.
 intros b c Hc H.
@@ -772,7 +831,7 @@ Qed.
 
 (** * Rational to the n-th power *)
 
-Definition Qpower_positive (q:Q)(p:positive) : Q := 
+Definition Qpower_positive (q:Q)(p:positive) : Q :=
  pow_pos Qmult q p.
 
 Add Morphism Qpower_positive with signature Qeq ==> @eq _ ==> Qeq as Qpower_positive_comp.
diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v
index 2e51ef973..5373c1db3 100644
--- a/theories/QArith/Qfield.v
+++ b/theories/QArith/Qfield.v
@@ -14,24 +14,9 @@ Require Import NArithRing.
 
 (** * field and ring tactics for rational numbers *)
 
-Definition Qeq_bool (x y : Q) :=
-  if Qeq_dec x y then true else false.
-
-Lemma Qeq_bool_correct : forall x y : Q, Qeq_bool x y = true -> x==y.
-Proof.
-  intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto.
-  intros _ H; inversion H.
-Qed.
-
-Lemma Qeq_bool_complete : forall x y : Q, x==y -> Qeq_bool x y = true.
-Proof.
-  intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto.
-Qed.
-
-Definition Qsft : field_theory 0 1 Qplus Qmult Qminus Qopp Qdiv Qinv Qeq.
+Definition Qsrt : ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq.
 Proof.
   constructor.
-  constructor.
   exact Qplus_0_l.
   exact Qplus_comm.
   exact Qplus_assoc.
@@ -41,6 +26,12 @@ Proof.
   exact Qmult_plus_distr_l.
   reflexivity.
   exact Qplus_opp_r.
+Qed.
+
+Definition Qsft : field_theory 0 1 Qplus Qmult Qminus Qopp Qdiv Qinv Qeq.
+Proof.
+  constructor.
+  exact Qsrt.
   discriminate.
   reflexivity.
   intros p Hp.
@@ -83,8 +74,8 @@ Ltac Qpow_tac t :=
   end.
 
 Add Field Qfield : Qsft 
- (decidable Qeq_bool_correct, 
-  completeness Qeq_bool_complete,
+ (decidable Qeq_bool_eq, 
+  completeness Qeq_eq_bool,
   constants [Qcst], 
   power_tac Qpower_theory [Qpow_tac]).
 
diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v
index c47f59385..cce0438fa 100644
--- a/theories/ZArith/Zbool.v
+++ b/theories/ZArith/Zbool.v
@@ -16,7 +16,7 @@ Require Import ZArith_dec.
 Require Import Sumbool.
 
 Unset Boxed Definitions.
-
+Open Local Scope Z_scope.
 
 (** * Boolean operations from decidabilty of order *)
 (** The decidability of equality and order relations over
@@ -37,80 +37,82 @@ Definition Zeven_odd_bool (x:Z) := bool_of_sumbool (Zeven_odd_dec x).
 (** * Boolean comparisons of binary integers *)
 
 Definition Zle_bool (x y:Z) :=
-  match (x ?= y)%Z with
+  match x ?= y with
     | Gt => false
     | _ => true
   end.
 
 Definition Zge_bool (x y:Z) :=
-  match (x ?= y)%Z with
+  match x ?= y with
     | Lt => false
     | _ => true
   end.
 
 Definition Zlt_bool (x y:Z) :=
-  match (x ?= y)%Z with
+  match x ?= y with
     | Lt => true
     | _ => false
   end.
 
 Definition Zgt_bool (x y:Z) :=
-  match (x ?= y)%Z with
+  match x ?= y with
     | Gt => true
     | _ => false
   end.
 
 Definition Zeq_bool (x y:Z) :=
-  match (x ?= y)%Z with
+  match x ?= y with
     | Eq => true
     | _ => false
   end.
 
 Definition Zneq_bool (x y:Z) :=
-  match (x ?= y)%Z with
+  match x ?= y with
     | Eq => false
     | _ => true
   end.
 
+(** Properties in term of [if ... then ... else ...] *)
+
 Lemma Zle_cases :
-  forall n m:Z, if Zle_bool n m then (n <= m)%Z else (n > m)%Z.
+  forall n m:Z, if Zle_bool n m then (n <= m) else (n > m).
 Proof.
   intros x y; unfold Zle_bool, Zle, Zgt in |- *.
-  case (x ?= y)%Z; auto; discriminate.
+  case (x ?= y); auto; discriminate.
 Qed.
 
 Lemma Zlt_cases :
-  forall n m:Z, if Zlt_bool n m then (n < m)%Z else (n >= m)%Z.
+  forall n m:Z, if Zlt_bool n m then (n < m) else (n >= m).
 Proof.
   intros x y; unfold Zlt_bool, Zlt, Zge in |- *.
-  case (x ?= y)%Z; auto; discriminate.
+  case (x ?= y); auto; discriminate.
 Qed.
 
 Lemma Zge_cases :
-  forall n m:Z, if Zge_bool n m then (n >= m)%Z else (n < m)%Z.
+  forall n m:Z, if Zge_bool n m then (n >= m) else (n < m).
 Proof.
   intros x y; unfold Zge_bool, Zge, Zlt in |- *.
-  case (x ?= y)%Z; auto; discriminate.
+  case (x ?= y); auto; discriminate.
 Qed.
 
 Lemma Zgt_cases :
-  forall n m:Z, if Zgt_bool n m then (n > m)%Z else (n <= m)%Z.
+  forall n m:Z, if Zgt_bool n m then (n > m) else (n <= m).
 Proof.
   intros x y; unfold Zgt_bool, Zgt, Zle in |- *.
-  case (x ?= y)%Z; auto; discriminate.
+  case (x ?= y); auto; discriminate.
 Qed.
 
 (** Lemmas on [Zle_bool] used in contrib/graphs *)
 
-Lemma Zle_bool_imp_le : forall n m:Z, Zle_bool n m = true -> (n <= m)%Z.
+Lemma Zle_bool_imp_le : forall n m:Z, Zle_bool n m = true -> (n <= m).
 Proof.
   unfold Zle_bool, Zle in |- *. intros x y. unfold not in |- *.
-  case (x ?= y)%Z; intros; discriminate.
+  case (x ?= y); intros; discriminate.
 Qed.
 
-Lemma Zle_imp_le_bool : forall n m:Z, (n <= m)%Z -> Zle_bool n m = true.
+Lemma Zle_imp_le_bool : forall n m:Z, (n <= m) -> Zle_bool n m = true.
 Proof.
-  unfold Zle, Zle_bool in |- *. intros x y. case (x ?= y)%Z; trivial. intro. elim (H (refl_equal _)).
+  unfold Zle, Zle_bool in |- *. intros x y. case (x ?= y); trivial. intro. elim (H (refl_equal _)).
 Qed.
 
 Lemma Zle_bool_refl : forall n:Z, Zle_bool n n = true.
@@ -136,8 +138,8 @@ Qed.
 Definition Zle_bool_total :
   forall x y:Z, {Zle_bool x y = true} + {Zle_bool y x = true}.
 Proof.
-  intros x y; intros. unfold Zle_bool in |- *. cut ((x ?= y)%Z = Gt <-> (y ?= x)%Z = Lt).
-  case (x ?= y)%Z. left. reflexivity.
+  intros x y; intros. unfold Zle_bool in |- *. cut ((x ?= y) = Gt <-> (y ?= x) = Lt).
+  case (x ?= y). left. reflexivity.
   left. reflexivity.
   right. rewrite (proj1 H (refl_equal _)). reflexivity.
   apply Zcompare_Gt_Lt_antisym.
@@ -159,39 +161,40 @@ Qed.
 
 Lemma Zone_min_pos : forall n:Z, Zle_bool n 0 = false -> Zle_bool 1 n = true.
 Proof.
-  intros x; intros. apply Zle_imp_le_bool. change (Zsucc 0 <= x)%Z in |- *. apply Zgt_le_succ. generalize H.
-  unfold Zle_bool, Zgt in |- *. case (x ?= 0)%Z. intro H0. discriminate H0.
+  intros x; intros. apply Zle_imp_le_bool. change (Zsucc 0 <= x) in |- *. apply Zgt_le_succ. generalize H.
+  unfold Zle_bool, Zgt in |- *. case (x ?= 0). intro H0. discriminate H0.
   intro H0. discriminate H0.
   reflexivity.
 Qed.
 
+(** Properties in term of [iff] *)
 
-Lemma Zle_is_le_bool : forall n m:Z, (n <= m)%Z <-> Zle_bool n m = true.
+Lemma Zle_is_le_bool : forall n m:Z, (n <= m) <-> Zle_bool n m = true.
 Proof.
   intros. split. intro. apply Zle_imp_le_bool. assumption.
   intro. apply Zle_bool_imp_le. assumption.
 Qed.
 
-Lemma Zge_is_le_bool : forall n m:Z, (n >= m)%Z <-> Zle_bool m n = true.
+Lemma Zge_is_le_bool : forall n m:Z, (n >= m) <-> Zle_bool m n = true.
 Proof.
   intros. split. intro. apply Zle_imp_le_bool. apply Zge_le. assumption.
   intro. apply Zle_ge. apply Zle_bool_imp_le. assumption.
 Qed.
 
-Lemma Zlt_is_lt_bool : forall n m:Z, (n < m)%Z <-> Zlt_bool n m = true.
+Lemma Zlt_is_lt_bool : forall n m:Z, (n < m) <-> Zlt_bool n m = true.
 Proof.
 intros n m; unfold Zlt_bool, Zlt.
-destruct (n ?= m)%Z; simpl; split; now intro.
+destruct (n ?= m); simpl; split; now intro.
 Qed.
 
-Lemma Zgt_is_gt_bool : forall n m:Z, (n > m)%Z <-> Zgt_bool n m = true.
+Lemma Zgt_is_gt_bool : forall n m:Z, (n > m) <-> Zgt_bool n m = true.
 Proof.
 intros n m; unfold Zgt_bool, Zgt.
-destruct (n ?= m)%Z; simpl; split; now intro.
+destruct (n ?= m); simpl; split; now intro.
 Qed.
 
 Lemma Zlt_is_le_bool :
-  forall n m:Z, (n < m)%Z <-> Zle_bool n (m - 1) = true.
+  forall n m:Z, (n < m) <-> Zle_bool n (m - 1) = true.
 Proof.
   intros x y. split. intro. apply Zle_imp_le_bool. apply Zlt_succ_le. rewrite (Zsucc_pred y) in H.
   assumption.
@@ -199,9 +202,29 @@ Proof.
 Qed.
 
 Lemma Zgt_is_le_bool :
-  forall n m:Z, (n > m)%Z <-> Zle_bool m (n - 1) = true.
+  forall n m:Z, (n > m) <-> Zle_bool m (n - 1) = true.
 Proof.
-  intros x y. apply iff_trans with (y < x)%Z. split. exact (Zgt_lt x y).
+  intros x y. apply iff_trans with (y < x). split. exact (Zgt_lt x y).
   exact (Zlt_gt y x).
   exact (Zlt_is_le_bool y x).
 Qed.
+
+Lemma Zeq_is_eq_bool : forall x y, x = y <-> Zeq_bool x y = true.
+Proof.
+  intros; unfold Zeq_bool.
+  generalize (Zcompare_Eq_iff_eq x y); destruct Zcompare; intuition;
+   try discriminate.
+Qed.
+
+Lemma Zeq_bool_eq : forall x y, Zeq_bool x y = true -> x = y.
+Proof.
+  intros x y H; apply <- Zeq_is_eq_bool; auto.
+Qed.
+
+Lemma Zeq_bool_neq : forall x y, Zeq_bool x y = false -> x <> y.
+Proof.
+  unfold Zeq_bool; red ; intros; subst.
+  rewrite Zcompare_refl in H.
+  discriminate.
+Qed.
+
diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v
index 6c5b07d24..8244d4ceb 100644
--- a/theories/ZArith/Zcompare.v
+++ b/theories/ZArith/Zcompare.v
@@ -40,6 +40,15 @@ Proof.
 	    | destruct ((x' ?= y')%positive Eq); reflexivity || discriminate ] ].
 Qed.
 
+Ltac destr_zcompare := 
+ match goal with |- context [Zcompare ?x ?y] => 
+  let H := fresh "H" in 
+  case_eq (Zcompare x y); intro H;
+   [generalize (Zcompare_Eq_eq _ _ H); clear H; intro H |
+    change (x<y)%Z in H | 
+    change (x>y)%Z in H ]
+ end.
+
 Lemma Zcompare_Eq_iff_eq : forall n m:Z, (n ?= m) = Eq <-> n = m.
 Proof.
   intros x y; split; intro E;