Imported Upstream snapshot 8.3~beta0+13298

3 files changed, 597 insertions, 533 deletions

diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index f01cbbc5..0bc71166 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -5,12 +5,13 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
-(************************************************************************)
 
-(*i $Id: BigQ.v 12509 2009-11-12 15:52:50Z letouzey $ i*)
+(** * BigQ: an efficient implementation of rational numbers *)
+
+(** Initial authors: Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
 
-Require Import Field Qfield BigN BigZ QSig QMake.
+Require Export BigZ.
+Require Import Field Qfield QSig QMake Orders GenericMinMax.
 
 (** We choose for BigQ an implemention with
     multiple representation of 0: 0, 1/0, 2/0 etc.
@@ -34,7 +35,9 @@ End BigN_BigZ.
 
 (** This allows to build [BigQ] out of [BigN] and [BigQ] via [QMake] *)
 
-Module BigQ <: QSig.QType := QMake.Make BigN BigZ BigN_BigZ.
+Module BigQ <: QType <: OrderedTypeFull <: TotalOrder :=
+ QMake.Make BigN BigZ BigN_BigZ <+ !QProperties <+ HasEqBool2Dec
+ <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties.
 
 (** Notations about [BigQ] *)
 
@@ -43,12 +46,40 @@ Notation bigQ := BigQ.t.
 Delimit Scope bigQ_scope with bigQ.
 Bind Scope bigQ_scope with bigQ.
 Bind Scope bigQ_scope with BigQ.t.
-
-(* Allow nice printing of rational numerals, either as (Qz 1234)
-   or as (Qq 1234 5678) *)
+Bind Scope bigQ_scope with BigQ.t_.
+(* Bind Scope has no retroactive effect, let's declare scopes by hand. *)
 Arguments Scope BigQ.Qz [bigZ_scope].
-Arguments Scope BigQ.Qq [bigZ_scope bigN_scope].			     
-			     
+Arguments Scope BigQ.Qq [bigZ_scope bigN_scope].
+Arguments Scope BigQ.to_Q [bigQ_scope].
+Arguments Scope BigQ.red [bigQ_scope].
+Arguments Scope BigQ.opp [bigQ_scope].
+Arguments Scope BigQ.inv [bigQ_scope].
+Arguments Scope BigQ.square [bigQ_scope].
+Arguments Scope BigQ.add [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.sub [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.mul [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.div [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.eq [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.lt [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.le [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.eq [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.compare [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.min [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.max [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.eq_bool [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.power_pos [bigQ_scope positive_scope].
+Arguments Scope BigQ.power [bigQ_scope Z_scope].
+Arguments Scope BigQ.inv_norm [bigQ_scope].
+Arguments Scope BigQ.add_norm [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.sub_norm [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.mul_norm [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.div_norm [bigQ_scope bigQ_scope].
+Arguments Scope BigQ.power_norm [bigQ_scope bigQ_scope].
+
+(** As in QArith, we use [#] to denote fractions *)
+Notation "p # q" := (BigQ.Qq p q) (at level 55, no associativity) : bigQ_scope.
+Local Notation "0" := BigQ.zero : bigQ_scope.
+Local Notation "1" := BigQ.one : bigQ_scope.
 Infix "+" := BigQ.add : bigQ_scope.
 Infix "-" := BigQ.sub : bigQ_scope.
 Notation "- x" := (BigQ.opp x) : bigQ_scope.
@@ -57,142 +88,102 @@ Infix "/" := BigQ.div : bigQ_scope.
 Infix "^" := BigQ.power : bigQ_scope.
 Infix "?=" := BigQ.compare : bigQ_scope.
 Infix "==" := BigQ.eq : bigQ_scope.
+Notation "x != y" := (~x==y)%bigQ (at level 70, no associativity) : bigQ_scope.
 Infix "<" := BigQ.lt : bigQ_scope.
 Infix "<=" := BigQ.le : 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 "x < y < z" := (x<y /\ y<z)%bigQ : bigQ_scope.
+Notation "x < y <= z" := (x<y /\ y<=z)%bigQ : bigQ_scope.
+Notation "x <= y < z" := (x<=y /\ y<z)%bigQ : bigQ_scope.
+Notation "x <= y <= z" := (x<=y /\ y<=z)%bigQ : bigQ_scope.
 Notation "[ q ]" := (BigQ.to_Q q) : bigQ_scope.
 
-Open Scope bigQ_scope.
-
-(** [BigQ] is a setoid *)
-
-Add Relation BigQ.t BigQ.eq
- reflexivity proved by (fun x => Qeq_refl [x])
- symmetry proved by (fun x y => Qeq_sym [x] [y])
- transitivity proved by (fun x y z => Qeq_trans [x] [y] [z])
-as BigQeq_rel.
-
-Add Morphism BigQ.add with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQadd_wd.
-Proof.
- unfold BigQ.eq; intros; rewrite !BigQ.spec_add; rewrite H, H0; apply Qeq_refl.
-Qed.
-
-Add Morphism BigQ.opp with signature BigQ.eq ==> BigQ.eq as BigQopp_wd.
-Proof.
- unfold BigQ.eq; intros; rewrite !BigQ.spec_opp; rewrite H; apply Qeq_refl.
-Qed.
-
-Add Morphism BigQ.sub with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQsub_wd.
-Proof.
- unfold BigQ.eq; intros; rewrite !BigQ.spec_sub; rewrite H, H0; apply Qeq_refl.
-Qed.
-
-Add Morphism BigQ.mul with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQmul_wd.
-Proof.
- unfold BigQ.eq; intros; rewrite !BigQ.spec_mul; rewrite H, H0; apply Qeq_refl.
-Qed.
-
-Add Morphism BigQ.inv with signature BigQ.eq ==> BigQ.eq as BigQinv_wd.
-Proof.
- unfold BigQ.eq; intros; rewrite !BigQ.spec_inv; rewrite H; apply Qeq_refl.
-Qed.
-
-Add Morphism BigQ.div with signature BigQ.eq ==> BigQ.eq ==> BigQ.eq as BigQdiv_wd.
-Proof.
- unfold BigQ.eq; intros; rewrite !BigQ.spec_div; rewrite H, H0; apply Qeq_refl.
-Qed.
-
-(* TODO : fix this. For the moment it's useless (horribly slow)
-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_mul BigQ.spec_inv BigQ.spec_div BigQ.spec_power_pos
- BigQ.spec_square : bigq. *)
-
+Local Open Scope bigQ_scope.
 
 (** [BigQ] is a field *)
 
 Lemma BigQfieldth :
- field_theory BigQ.zero BigQ.one BigQ.add BigQ.mul BigQ.sub BigQ.opp BigQ.div BigQ.inv BigQ.eq.
+ field_theory 0 1 BigQ.add BigQ.mul BigQ.sub BigQ.opp
+  BigQ.div BigQ.inv BigQ.eq.
 Proof.
 constructor.
-constructor; intros; red.
-rewrite BigQ.spec_add, BigQ.spec_0; ring.
-rewrite ! BigQ.spec_add; ring.
-rewrite ! BigQ.spec_add; ring.
-rewrite BigQ.spec_mul, BigQ.spec_1; ring.
-rewrite ! BigQ.spec_mul; ring.
-rewrite ! BigQ.spec_mul; ring.
-rewrite BigQ.spec_add, ! BigQ.spec_mul, BigQ.spec_add; ring.
-unfold BigQ.sub; apply Qeq_refl.
-rewrite BigQ.spec_add, BigQ.spec_0, BigQ.spec_opp; ring.
-compute; discriminate.
-intros; red.
-unfold BigQ.div; apply Qeq_refl.
-intros; red.
-rewrite BigQ.spec_mul, BigQ.spec_inv, BigQ.spec_1; field.
-rewrite <- BigQ.spec_0; auto.
-Qed.
-
-Lemma BigQpowerth :
- power_theory BigQ.one BigQ.mul BigQ.eq Z_of_N BigQ.power.
-Proof.
 constructor.
-intros; red.
-rewrite BigQ.spec_power.
-replace ([r] ^ Z_of_N n)%Q with (pow_N 1 Qmult [r] n)%Q.
-destruct n.
-simpl; compute; auto.
-induction p; simpl; auto; try rewrite !BigQ.spec_mul, !IHp; apply Qeq_refl.
-destruct n; reflexivity.
-Qed.
-
-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.
+exact BigQ.add_0_l. exact BigQ.add_comm. exact BigQ.add_assoc.
+exact BigQ.mul_1_l. exact BigQ.mul_comm. exact BigQ.mul_assoc.
+exact BigQ.mul_add_distr_r. exact BigQ.sub_add_opp.
+exact BigQ.add_opp_diag_r. exact BigQ.neq_1_0.
+exact BigQ.div_mul_inv. exact BigQ.mul_inv_diag_l.
 Qed.
 
-Lemma BigQ_eq_bool_complete :
- forall x y, x==y -> BigQ.eq_bool x y = true.
+Lemma BigQpowerth :
+ power_theory 1 BigQ.mul BigQ.eq Z_of_N BigQ.power.
 Proof.
-intros; generalize (BigQ.spec_eq_bool x y).
-destruct BigQ.eq_bool; auto.
+constructor. intros. BigQ.qify.
+replace ([r] ^ Z_of_N n)%Q with (pow_N 1 Qmult [r] n)%Q by (now destruct n).
+destruct n. reflexivity.
+induction p; simpl; auto; rewrite ?BigQ.spec_mul, ?IHp; reflexivity.
 Qed.
 
-(* TODO : improve later the detection of constants ... *)
+Ltac isBigQcst t :=
+ match t with
+ | BigQ.Qz ?t => isBigZcst t
+ | BigQ.Qq ?n ?d => match isBigZcst n with
+             | true => isBigNcst d
+             | false => constr:false
+             end
+ | BigQ.zero => constr:true
+ | BigQ.one => constr:true
+ | BigQ.minus_one => constr:true
+ | _ => constr:false
+ end.
 
 Ltac BigQcst t :=
- match t with
-   | BigQ.zero => BigQ.zero
-   | BigQ.one => BigQ.one
-   | BigQ.minus_one => BigQ.minus_one
-   | _ => NotConstant
+ match isBigQcst t with
+ | true => constr:t
+ | false => constr:NotConstant
  end.
 
 Add Field BigQfield : BigQfieldth
- (decidable BigQ_eq_bool_correct,
-  completeness BigQ_eq_bool_complete,
+ (decidable BigQ.eqb_correct,
+  completeness BigQ.eqb_complete,
   constants [BigQcst],
   power_tac BigQpowerth [Qpow_tac]).
 
-Section Examples.
+Section TestField.
 
 Let ex1 : forall x y z, (x+y)*z ==  (x*z)+(y*z).
   intros.
   ring.
 Qed.
 
-Let ex8 : forall x, x ^ 1 == x.
+Let ex8 : forall x, x ^ 2 == x*x.
   intro.
   ring.
 Qed.
 
-Let ex10 : forall x y, ~(y==BigQ.zero) -> (x/y)*y == x.
+Let ex10 : forall x y, y!=0 -> (x/y)*y == x.
 intros.
 field.
 auto.
 Qed.
 
-End Examples.
\ No newline at end of file
+End TestField.
+
+(** [BigQ] can also benefit from an "order" tactic *)
+
+Module BigQ_Order := !OrdersTac.MakeOrderTac BigQ.
+Ltac bigQ_order := BigQ_Order.order.
+
+Section TestOrder.
+Let test : forall x y : bigQ, x<=y -> y<=x -> x==y.
+Proof. bigQ_order. Qed.
+End TestOrder.
+
+(** We can also reason by switching to QArith thanks to tactic
+    BigQ.qify. *)
+
+Section TestQify.
+Let test : forall x : bigQ, 0+x == 1*x.
+Proof. intro x. BigQ.qify. ring. Qed.
+End TestQify.
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index 494420bd..407f7b90 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -5,15 +5,20 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(*            Benjamin Gregoire, Laurent Thery, INRIA, 2007             *)
-(************************************************************************)
 
-(*i $Id: QMake.v 11208 2008-07-04 16:57:46Z letouzey $ i*)
+(** * QMake : a generic efficient implementation of rational numbers *)
+
+(** Initial authors : Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
 
 Require Import BigNumPrelude ROmega.
-Require Import QArith Qcanon Qpower.
+Require Import QArith Qcanon Qpower Qminmax.
 Require Import NSig ZSig QSig.
 
+(** We will build rationals out of an implementation of integers [ZType]
+    for numerators and an implementation of natural numbers [NType] for
+    denominators. But first we will need some glue between [NType] and
+    [ZType]. *)
+
 Module Type NType_ZType (N:NType)(Z:ZType).
  Parameter Z_of_N : N.t -> Z.t.
  Parameter spec_Z_of_N : forall n, Z.to_Z (Z_of_N n) = N.to_Z n.
@@ -28,27 +33,27 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
      number y interpreted as x/y. The pairs (x,0) and (0,y) are all
      interpreted as 0. *)
 
- Inductive t_ := 
+ Inductive t_ :=
   | Qz : Z.t -> t_
   | Qq : Z.t -> N.t -> t_.
 
  Definition t := t_.
 
- (** Specification with respect to [QArith] *) 
+ (** Specification with respect to [QArith] *)
 
- Open Local Scope Q_scope.
+ Local Open Scope Q_scope.
 
  Definition of_Z x: t := Qz (Z.of_Z x).
 
- Definition of_Q (q:Q) : t := 
-  let (x,y) := q in 
-  match y with 
+ Definition of_Q (q:Q) : t :=
+  let (x,y) := q in
+  match y with
     | 1%positive => Qz (Z.of_Z x)
     | _ => Qq (Z.of_Z x) (N.of_N (Npos y))
   end.
 
- Definition to_Q (q: t) := 
- match q with 
+ Definition to_Q (q: t) :=
+ match q with
    | Qz x => Z.to_Z x # 1
    | Qq x y => if N.eq_bool y N.zero then 0
                else Z.to_Z x # Z2P (N.to_Z y)
@@ -56,17 +61,56 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Notation "[ x ]" := (to_Q x).
 
+ Lemma N_to_Z_pos :
+  forall x, (N.to_Z x <> N.to_Z N.zero)%Z -> (0 < N.to_Z x)%Z.
+ Proof.
+ intros x; rewrite N.spec_0; generalize (N.spec_pos x). romega.
+ Qed.
+(*
+ Lemma if_fun_commut : forall A B (f:A->B)(b:bool) a a',
+ f (if b then a else a') = if b then f a else f a'.
+ Proof. now destruct b. Qed.
+
+ Lemma if_fun_commut' : forall A B C D (f:A->B)(b:{C}+{D}) a a',
+ f (if b then a else a') = if b then f a else f a'.
+ Proof. now destruct b. Qed.
+*)
+ Ltac destr_eqb :=
+  match goal with
+   | |- context [Z.eq_bool ?x ?y] =>
+     rewrite (Z.spec_eq_bool x y);
+     generalize (Zeq_bool_if (Z.to_Z x) (Z.to_Z y));
+     case (Zeq_bool (Z.to_Z x) (Z.to_Z y));
+     destr_eqb
+   | |- context [N.eq_bool ?x ?y] =>
+     rewrite (N.spec_eq_bool x y);
+     generalize (Zeq_bool_if (N.to_Z x) (N.to_Z y));
+     case (Zeq_bool (N.to_Z x) (N.to_Z y));
+     [ | let H:=fresh "H" in
+         try (intro H;generalize (N_to_Z_pos _ H); clear H)];
+     destr_eqb
+   | _ => idtac
+  end.
+
+ Hint Rewrite
+  Zplus_0_r Zplus_0_l Zmult_0_r Zmult_0_l Zmult_1_r Zmult_1_l
+  Z.spec_0 N.spec_0 Z.spec_1 N.spec_1 Z.spec_m1 Z.spec_opp
+  Z.spec_compare N.spec_compare
+  Z.spec_add N.spec_add Z.spec_mul N.spec_mul Z.spec_div N.spec_div
+  Z.spec_gcd N.spec_gcd Zgcd_Zabs Zgcd_1
+  spec_Z_of_N spec_Zabs_N
+ : nz.
+ Ltac nzsimpl := autorewrite with nz in *.
+
+ Ltac qsimpl := try red; unfold to_Q; simpl; intros;
+  destr_eqb; simpl; nzsimpl; intros;
+  rewrite ?Z2P_correct by auto;
+  auto.
+
  Theorem strong_spec_of_Q: forall q: Q, [of_Q q] = q.
  Proof.
- intros(x,y); destruct y; simpl; rewrite Z.spec_of_Z; auto.
- generalize (N.spec_eq_bool (N.of_N (Npos y~1)) N.zero); 
-  case N.eq_bool; auto; rewrite N.spec_0.
- rewrite N.spec_of_N; intros; discriminate.
- rewrite N.spec_of_N; auto.
- generalize (N.spec_eq_bool (N.of_N (Npos y~0)) N.zero); 
-  case N.eq_bool; auto; rewrite N.spec_0.
- rewrite N.spec_of_N; intros; discriminate.
- rewrite N.spec_of_N; auto.
+ intros(x,y); destruct y; simpl; rewrite ?Z.spec_of_Z; auto;
+  destr_eqb; now rewrite ?N.spec_0, ?N.spec_of_N.
  Qed.
 
  Theorem spec_of_Q: forall q: Q, [of_Q q] == q.
@@ -82,131 +126,96 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Lemma spec_0: [zero] == 0.
  Proof.
- simpl; rewrite Z.spec_0; reflexivity.
+ simpl. nzsimpl. reflexivity.
  Qed.
 
  Lemma spec_1: [one] == 1.
  Proof.
- simpl; rewrite Z.spec_1; reflexivity.
+ simpl. nzsimpl. reflexivity.
  Qed.
 
  Lemma spec_m1: [minus_one] == -(1).
  Proof.
- simpl; rewrite Z.spec_m1; reflexivity.
+ simpl. nzsimpl. reflexivity.
  Qed.
 
  Definition compare (x y: t) :=
   match x, y with
   | Qz zx, Qz zy => Z.compare zx zy
-  | Qz zx, Qq ny dy => 
+  | Qz zx, Qq ny dy =>
     if N.eq_bool dy N.zero then Z.compare zx Z.zero
     else Z.compare (Z.mul zx (Z_of_N dy)) ny
-  | Qq nx dx, Qz zy => 
-    if N.eq_bool dx N.zero then Z.compare Z.zero zy 
+  | Qq nx dx, Qz zy =>
+    if N.eq_bool dx N.zero then Z.compare Z.zero zy
     else Z.compare nx (Z.mul zy (Z_of_N dx))
   | Qq nx dx, Qq ny dy =>
     match N.eq_bool dx N.zero, N.eq_bool dy N.zero with
     | true, true => Eq
     | true, false => Z.compare Z.zero ny
     | false, true => Z.compare nx Z.zero
-    | false, false => Z.compare (Z.mul nx (Z_of_N dy)) 
+    | false, false => Z.compare (Z.mul nx (Z_of_N dy))
                                 (Z.mul ny (Z_of_N dx))
     end
   end.
 
- Lemma Zcompare_spec_alt : 
-  forall z z', Z.compare z z' = (Z.to_Z z ?= Z.to_Z z')%Z.
+ Theorem spec_compare: forall q1 q2, (compare q1 q2) = ([q1] ?= [q2]).
  Proof.
- intros; generalize (Z.spec_compare z z'); destruct Z.compare; auto.
- intro H; rewrite H; symmetry; apply Zcompare_refl.
+ intros [z1 | x1 y1] [z2 | x2 y2];
+   unfold Qcompare, compare; qsimpl.
  Qed.
- 
- Lemma Ncompare_spec_alt : 
-  forall n n', N.compare n n' = (N.to_Z n ?= N.to_Z n')%Z.
+
+ Definition lt n m := [n] < [m].
+ Definition le n m := [n] <= [m].
+
+ Definition min n m := match compare n m with Gt => m | _ => n end.
+ Definition max n m := match compare n m with Lt => m | _ => n end.
+
+ Lemma spec_min : forall n m, [min n m] == Qmin [n] [m].
  Proof.
- intros; generalize (N.spec_compare n n'); destruct N.compare; auto.
- intro H; rewrite H; symmetry; apply Zcompare_refl.
+ unfold min, Qmin, GenericMinMax.gmin. intros.
+ rewrite spec_compare; destruct Qcompare; auto with qarith.
  Qed.
 
- Lemma N_to_Z2P : forall n, N.to_Z n <> 0%Z -> 
-  Zpos (Z2P (N.to_Z n)) = N.to_Z n.
+ Lemma spec_max : forall n m, [max n m] == Qmax [n] [m].
  Proof.
- intros; apply Z2P_correct.
- generalize (N.spec_pos n); romega.
+ unfold max, Qmax, GenericMinMax.gmax. intros.
+ rewrite spec_compare; destruct Qcompare; auto with qarith.
  Qed.
 
- Hint Rewrite 
-  Zplus_0_r Zplus_0_l Zmult_0_r Zmult_0_l Zmult_1_r Zmult_1_l 
-  Z.spec_0 N.spec_0 Z.spec_1 N.spec_1 Z.spec_m1 Z.spec_opp
-  Zcompare_spec_alt Ncompare_spec_alt
-  Z.spec_add N.spec_add Z.spec_mul N.spec_mul 
-  Z.spec_gcd N.spec_gcd Zgcd_Zabs
-  spec_Z_of_N spec_Zabs_N
- : nz.
- Ltac nzsimpl := autorewrite with nz in *.
-
- Ltac destr_neq_bool := repeat
- (match goal with |- context [N.eq_bool ?x ?y] => 
-   generalize (N.spec_eq_bool x y); case N.eq_bool
-  end).
- 
- Ltac destr_zeq_bool := repeat
- (match goal with |- context [Z.eq_bool ?x ?y] => 
-   generalize (Z.spec_eq_bool x y); case Z.eq_bool
-  end).
-
- Ltac simpl_ndiv := rewrite N.spec_div by (nzsimpl; romega).
- Tactic Notation "simpl_ndiv" "in" "*" := 
-   rewrite N.spec_div in * by (nzsimpl; romega).
-
- Ltac simpl_zdiv := rewrite Z.spec_div by (nzsimpl; romega).
- Tactic Notation "simpl_zdiv" "in" "*" := 
-   rewrite Z.spec_div in * by (nzsimpl; romega).
-
- Ltac qsimpl := try red; unfold to_Q; simpl; intros; 
-  destr_neq_bool; destr_zeq_bool; simpl; nzsimpl; auto; intros.
+ Definition eq_bool n m :=
+  match compare n m with Eq => true | _ => false end.
 
- Theorem spec_compare: forall q1 q2, (compare q1 q2) = ([q1] ?= [q2]).
+ Theorem spec_eq_bool: forall x y, eq_bool x y = Qeq_bool [x] [y].
  Proof.
- intros [z1 | x1 y1] [z2 | x2 y2]; 
-   unfold Qcompare, compare; qsimpl; rewrite ! N_to_Z2P; auto.
+ intros. unfold eq_bool. rewrite spec_compare. reflexivity.
  Qed.
 
- Definition lt n m := compare n m = Lt.
- Definition le n m := compare n m <> Gt.
- Definition min n m := match compare n m with Gt => m | _ => n end.
- Definition max n m := match compare n m with Lt => m | _ => n end.
+ (** [check_int] : is a reduced fraction [n/d] in fact a integer ? *)
 
- Definition eq_bool n m := 
-  match compare n m with Eq => true | _ => false end.
+ Definition check_int n d :=
+  match N.compare N.one d with
+  | Lt => Qq n d
+  | Eq => Qz n
+  | Gt => zero  (* n/0 encodes 0 *)
+  end.
 
- Theorem spec_eq_bool: forall x y,
-  if eq_bool x y then [x] == [y] else ~([x] == [y]).
+ Theorem strong_spec_check_int : forall n d, [check_int n d] = [Qq n d].
  Proof.
- intros.
- unfold eq_bool.
- rewrite spec_compare.
- generalize (Qeq_alt [x] [y]).
- destruct Qcompare.
- intros H; rewrite H; auto.
- intros H H'; rewrite H in H'; discriminate.
- intros H H'; rewrite H in H'; discriminate.
+ intros; unfold check_int.
+ nzsimpl.
+ destr_zcompare.
+ simpl. rewrite <- H; qsimpl. congruence.
+ reflexivity.
+ qsimpl. exfalso; romega.
  Qed.
 
  (** Normalisation function *)
 
  Definition norm n d : t :=
-  let gcd := N.gcd (Zabs_N n) d in 
+  let gcd := N.gcd (Zabs_N n) d in
   match N.compare N.one gcd with
-  | Lt => 
-    let n := Z.div n (Z_of_N gcd) in
-    let d := N.div d gcd in
-    match N.compare d N.one with
-    | Gt => Qq n d
-    | Eq => Qz n
-    | Lt => zero
-    end
-  | Eq => Qq n d
+  | Lt => check_int (Z.div n (Z_of_N gcd)) (N.div d gcd)
+  | Eq => check_int n d
   | Gt => zero (* gcd = 0 => both numbers are 0 *)
   end.
 
@@ -217,29 +226,16 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  assert (Hq := N.spec_pos q).
  nzsimpl.
  destr_zcompare.
+ (* Eq *)
+ rewrite strong_spec_check_int; reflexivity.
+ (* Lt *)
+ rewrite strong_spec_check_int.
  qsimpl.
-
- simpl_ndiv.
- destr_zcompare.
- qsimpl.
- rewrite H1 in *; rewrite Zdiv_0_l in H0; discriminate.
- rewrite N_to_Z2P; auto.
- simpl_zdiv; nzsimpl.
- rewrite Zgcd_div_swap0, H0; romega.
-
- qsimpl.
- assert (0 < N.to_Z q / Zgcd (Z.to_Z p) (N.to_Z q))%Z.
-  apply Zgcd_div_pos; romega.
- romega.
-
- qsimpl.
- simpl_ndiv in *; nzsimpl; romega.
- simpl_ndiv in *.
- rewrite H1, Zdiv_0_l in H2; elim H2; auto.
- rewrite 2 N_to_Z2P; auto.
- simpl_ndiv; simpl_zdiv; nzsimpl.
+ generalize (Zgcd_div_pos (Z.to_Z p) (N.to_Z q)). romega.
+ replace (N.to_Z q) with 0%Z in * by assumption.
+ rewrite Zdiv_0_l in *; auto with zarith.
  apply Zgcd_div_swap0; romega.
-
+ (* Gt *)
  qsimpl.
  assert (H' : Zgcd (Z.to_Z p) (N.to_Z q) = 0%Z).
   generalize (Zgcd_is_pos (Z.to_Z p) (N.to_Z q)); romega.
@@ -249,48 +245,37 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem strong_spec_norm : forall p q, [norm p q] = Qred [Qq p q].
  Proof.
  intros.
- replace (Qred [Qq p q]) with (Qred [norm p q]) by 
+ replace (Qred [Qq p q]) with (Qred [norm p q]) by
   (apply Qred_complete; apply spec_norm).
  symmetry; apply Qred_identity.
  unfold norm.
  assert (Hp := N.spec_pos (Zabs_N p)).
  assert (Hq := N.spec_pos q).
  nzsimpl.
- destr_zcompare.
+ destr_zcompare; rewrite ?strong_spec_check_int.
  (* Eq *)
- simpl.
- destr_neq_bool; nzsimpl; simpl; auto.
- intros.
- rewrite N_to_Z2P; auto.
- (* Lt *)
- simpl_ndiv.
- destr_zcompare.
- qsimpl; auto.
  qsimpl.
+ (* Lt *)
  qsimpl.
- simpl_zdiv; nzsimpl.
- rewrite N_to_Z2P; auto.
- clear H1.
- simpl_ndiv; nzsimpl.
  rewrite Zgcd_1_rel_prime.
  destruct (Z_lt_le_dec 0 (N.to_Z q)).
  apply Zis_gcd_rel_prime; auto with zarith.
  apply Zgcd_is_gcd.
  replace (N.to_Z q) with 0%Z in * by romega.
- rewrite Zdiv_0_l in H0; discriminate.
+ rewrite Zdiv_0_l in *; romega.
  (* Gt *)
- simpl; auto.
+ simpl; auto with zarith.
  Qed.
 
- (** Reduction function : producing irreducible fractions *) 
+ (** Reduction function : producing irreducible fractions *)
 
- Definition red (x : t) : t := 
-  match x with 
+ Definition red (x : t) : t :=
+  match x with
    | Qz z => x
    | Qq n d => norm n d
   end.
 
- Definition Reduced x := [red x] = [x].
+ Class Reduced x := is_reduced : [red x] = [x].
 
  Theorem spec_red : forall x, [red x] == [x].
  Proof.
@@ -304,21 +289,21 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Proof.
  intros [ z | n d ].
  unfold red.
- symmetry; apply Qred_identity; simpl; auto.
+ symmetry; apply Qred_identity; simpl; auto with zarith.
  unfold red; apply strong_spec_norm.
  Qed.
-   
+
  Definition add (x y: t): t :=
   match x with
   | Qz zx =>
     match y with
     | Qz zy => Qz (Z.add zx zy)
-    | Qq ny dy => 
-      if N.eq_bool dy N.zero then x 
+    | Qq ny dy =>
+      if N.eq_bool dy N.zero then x
       else Qq (Z.add (Z.mul zx (Z_of_N dy)) ny) dy
     end
   | Qq nx dx =>
-    if N.eq_bool dx N.zero then y 
+    if N.eq_bool dx N.zero then y
     else match y with
     | Qz zy => Qq (Z.add nx (Z.mul zy (Z_of_N dx))) dx
     | Qq ny dy =>
@@ -332,19 +317,12 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Theorem spec_add : forall x y, [add x y] == [x] + [y].
  Proof.
- intros [x | nx dx] [y | ny dy]; unfold Qplus; qsimpl.
- intuition.
- rewrite N_to_Z2P; auto.
- intuition.
- rewrite Pmult_1_r, N_to_Z2P; auto.
- intuition.
- rewrite Pmult_1_r, N_to_Z2P; auto.
- destruct (Zmult_integral _ _ H); intuition.
- rewrite Zpos_mult_morphism, 2 N_to_Z2P; auto.
- rewrite (Z2P_correct (N.to_Z dx * N.to_Z dy)); auto.
- apply Zmult_lt_0_compat.
-  generalize (N.spec_pos dx); romega.
-  generalize (N.spec_pos dy); romega.
+ intros [x | nx dx] [y | ny dy]; unfold Qplus; qsimpl;
+  auto with zarith.
+ rewrite Pmult_1_r, Z2P_correct; auto.
+ rewrite Pmult_1_r, Z2P_correct; auto.
+ destruct (Zmult_integral (N.to_Z dx) (N.to_Z dy)); intuition.
+ rewrite Zpos_mult_morphism, 2 Z2P_correct; auto.
  Qed.
 
  Definition add_norm (x y: t): t :=
@@ -352,12 +330,12 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
   | Qz zx =>
     match y with
     | Qz zy => Qz (Z.add zx zy)
-    | Qq ny dy =>  
-      if N.eq_bool dy N.zero then x 
+    | Qq ny dy =>
+      if N.eq_bool dy N.zero then x
       else norm (Z.add (Z.mul zx (Z_of_N dy)) ny) dy
     end
   | Qq nx dx =>
-    if N.eq_bool dx N.zero then y 
+    if N.eq_bool dx N.zero then y
     else match y with
     | Qz zy => norm (Z.add nx (Z.mul zy (Z_of_N dx))) dx
     | Qq ny dy =>
@@ -372,26 +350,20 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_add_norm : forall x y, [add_norm x y] == [x] + [y].
  Proof.
  intros x y; rewrite <- spec_add.
- destruct x; destruct y; unfold add_norm, add; 
- destr_neq_bool; auto using Qeq_refl, spec_norm.
+ destruct x; destruct y; unfold add_norm, add;
+ destr_eqb; auto using Qeq_refl, spec_norm.
  Qed.
 
- Theorem strong_spec_add_norm : forall x y : t, 
-   Reduced x -> Reduced y -> Reduced (add_norm x y).
+ Instance strong_spec_add_norm x y
+   `(Reduced x, Reduced y) : Reduced (add_norm x y).
  Proof.
  unfold Reduced; intros.
  rewrite strong_spec_red.
- rewrite <- (Qred_complete [add x y]); 
+ rewrite <- (Qred_complete [add x y]);
   [ | rewrite spec_add, spec_add_norm; apply Qeq_refl ].
  rewrite <- strong_spec_red.
- destruct x as [zx|nx dx]; destruct y as [zy|ny dy].
- simpl in *; auto.
- simpl; intros.
- destr_neq_bool; nzsimpl; simpl; auto.
- simpl; intros.
- destr_neq_bool; nzsimpl; simpl; auto.
- simpl; intros.
- destr_neq_bool; nzsimpl; simpl; auto.
+ destruct x as [zx|nx dx]; destruct y as [zy|ny dy];
+  simpl; destr_eqb; nzsimpl; simpl; auto.
  Qed.
 
  Definition opp (x: t): t :=
@@ -404,7 +376,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Proof.
  intros [z | x y]; simpl.
  rewrite Z.spec_opp; auto.
- match goal with  |- context[N.eq_bool ?X ?Y] => 
+ match goal with  |- context[N.eq_bool ?X ?Y] =>
   generalize (N.spec_eq_bool X Y); case N.eq_bool
  end; auto; rewrite N.spec_0.
  rewrite Z.spec_opp; auto.
@@ -415,7 +387,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  intros; rewrite strong_spec_opp; red; auto.
  Qed.
 
- Theorem strong_spec_opp_norm : forall q, Reduced q -> Reduced (opp q).
+ Instance strong_spec_opp_norm q `(Reduced q) : Reduced (opp q).
  Proof.
  unfold Reduced; intros.
  rewrite strong_spec_opp, <- H, !strong_spec_red, <- Qred_opp.
@@ -438,8 +410,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite spec_opp; ring.
  Qed.
 
- Theorem strong_spec_sub_norm : forall x y, 
-  Reduced x -> Reduced y -> Reduced (sub_norm x y).
+ Instance strong_spec_sub_norm x y
+  `(Reduced x, Reduced y) : Reduced (sub_norm x y).
  Proof.
  intros.
  unfold sub_norm.
@@ -458,35 +430,34 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_mul : forall x y, [mul x y] == [x] * [y].
  Proof.
  intros [x | nx dx] [y | ny dy]; unfold Qmult; simpl; qsimpl.
- rewrite Pmult_1_r, N_to_Z2P; auto.
- destruct (Zmult_integral _ _ H1); intuition.
- rewrite H0 in H1; elim H1; auto.
- rewrite H0 in H1; elim H1; auto.
- rewrite H in H1; nzsimpl; elim H1; auto.
- rewrite Zpos_mult_morphism, 2 N_to_Z2P; auto.
- rewrite (Z2P_correct (N.to_Z dx * N.to_Z dy)); auto.
- apply Zmult_lt_0_compat.
-  generalize (N.spec_pos dx); omega.
-  generalize (N.spec_pos dy); omega.
+ rewrite Pmult_1_r, Z2P_correct; auto.
+ destruct (Zmult_integral (N.to_Z dx) (N.to_Z dy)); intuition.
+ rewrite H0 in H1; auto with zarith.
+ rewrite H0 in H1; auto with zarith.
+ rewrite H in H1; nzsimpl; auto with zarith.
+ rewrite Zpos_mult_morphism, 2 Z2P_correct; auto.
  Qed.
 
- Lemma norm_denum : forall n d, 
-  [if N.eq_bool d N.one then Qz n else Qq n d] == [Qq n d].
+ Definition norm_denum n d :=
+  if N.eq_bool d N.one then Qz n else Qq n d.
+
+ Lemma spec_norm_denum : forall n d,
+  [norm_denum n d] == [Qq n d].
  Proof.
- intros; simpl; qsimpl.
- rewrite H0 in H; discriminate.
- rewrite N_to_Z2P, H0; auto with zarith.
+ unfold norm_denum; intros; simpl; qsimpl.
+ congruence.
+ rewrite H0 in *; auto with zarith.
  Qed.
 
- Definition irred n d :=        
+ Definition irred n d :=
    let gcd := N.gcd (Zabs_N n) d in
-   match N.compare gcd N.one with 
+   match N.compare gcd N.one with
      | Gt => (Z.div n (Z_of_N gcd), N.div d gcd)
      | _ => (n, d)
    end.
 
- Lemma spec_irred : forall n d, exists g, 
-  let (n',d') := irred n d in 
+ Lemma spec_irred : forall n d, exists g,
+  let (n',d') := irred n d in
   (Z.to_Z n' * g = Z.to_Z n)%Z /\ (N.to_Z d' * g = N.to_Z d)%Z.
  Proof.
  intros.
@@ -503,15 +474,15 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  exists (Zgcd (Z.to_Z n) (N.to_Z d)).
  simpl.
  split.
- simpl_zdiv; nzsimpl.
+ nzsimpl.
  destruct (Zgcd_is_gcd (Z.to_Z n) (N.to_Z d)).
  rewrite Zmult_comm; symmetry; apply Zdivide_Zdiv_eq; auto with zarith.
- simpl_ndiv; nzsimpl.
+ nzsimpl.
  destruct (Zgcd_is_gcd (Z.to_Z n) (N.to_Z d)).
  rewrite Zmult_comm; symmetry; apply Zdivide_Zdiv_eq; auto with zarith.
  Qed.
 
- Lemma spec_irred_zero : forall n d, 
+ Lemma spec_irred_zero : forall n d,
    (N.to_Z d = 0)%Z <-> (N.to_Z (snd (irred n d)) = 0)%Z.
  Proof.
  intros.
@@ -520,10 +491,10 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  nzsimpl; intros.
  destr_zcompare; auto.
  simpl.
- simpl_ndiv; nzsimpl.
+ nzsimpl.
  rewrite H, Zdiv_0_l; auto.
  nzsimpl; destr_zcompare; simpl; auto.
- simpl_ndiv; nzsimpl.
+ nzsimpl.
  intros.
  generalize (N.spec_pos d); intros.
  destruct (N.to_Z d); auto.
@@ -535,8 +506,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  compute in H1; elim H1; auto.
  Qed.
 
- Lemma strong_spec_irred : forall n d, 
-  (N.to_Z d <> 0%Z) -> 
+ Lemma strong_spec_irred : forall n d,
+  (N.to_Z d <> 0%Z) ->
   let (n',d') := irred n d in Zgcd (Z.to_Z n') (N.to_Z d') = 1%Z.
  Proof.
  unfold irred; intros.
@@ -546,7 +517,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  apply (Zgcd_inv_0_r (Z.to_Z n)).
  generalize (Zgcd_is_pos (Z.to_Z n) (N.to_Z d)); romega.
 
- simpl_ndiv; simpl_zdiv; nzsimpl.
+ nzsimpl.
  rewrite Zgcd_1_rel_prime.
  apply Zis_gcd_rel_prime.
  generalize (N.spec_pos d); romega.
@@ -554,89 +525,81 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  apply Zgcd_is_gcd; auto.
  Qed.
 
- Definition mul_norm_Qz_Qq z n d := 
-   if Z.eq_bool z Z.zero then zero 
+ Definition mul_norm_Qz_Qq z n d :=
+   if Z.eq_bool z Z.zero then zero
    else
     let gcd := N.gcd (Zabs_N z) d in
     match N.compare gcd N.one with
-      | Gt => 
+      | Gt =>
         let z := Z.div z (Z_of_N gcd) in
         let d := N.div d gcd in
-        if N.eq_bool d N.one then Qz (Z.mul z n) else Qq (Z.mul z n) d
+        norm_denum (Z.mul z n) d
       | _  => Qq (Z.mul z n) d
     end.
 
- Definition mul_norm (x y: t): t := 
+ Definition mul_norm (x y: t): t :=
  match x, y with
  | Qz zx, Qz zy => Qz (Z.mul zx zy)
  | Qz zx, Qq ny dy => mul_norm_Qz_Qq zx ny dy
  | Qq nx dx, Qz zy => mul_norm_Qz_Qq zy nx dx
- | Qq nx dx, Qq ny dy => 
-    let (nx, dy) := irred nx dy in 
-    let (ny, dx) := irred ny dx in 
-    let d := N.mul dx dy in
-    if N.eq_bool d N.one then Qz (Z.mul ny nx) else Qq (Z.mul ny nx) d
+ | Qq nx dx, Qq ny dy =>
+    let (nx, dy) := irred nx dy in
+    let (ny, dx) := irred ny dx in
+    norm_denum (Z.mul ny nx) (N.mul dx dy)
  end.
 
- Lemma spec_mul_norm_Qz_Qq : forall z n d, 
+ Lemma spec_mul_norm_Qz_Qq : forall z n d,
    [mul_norm_Qz_Qq z n d] == [Qq (Z.mul z n) d].
  Proof.
  intros z n d; unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt.
- destr_zeq_bool; intros Hz; nzsimpl.
+ destr_eqb; nzsimpl; intros Hz.
  qsimpl; rewrite Hz; auto.
- assert (Hd := N.spec_pos d).
- destruct Z_le_gt_dec.
+ destruct Z_le_gt_dec; intros.
  qsimpl.
- rewrite norm_denum.
+ rewrite spec_norm_denum.
  qsimpl.
- simpl_ndiv in *; nzsimpl.
- rewrite (Zdiv_gcd_zero _ _ H0 H) in z0; discriminate.
- simpl_ndiv in *; nzsimpl.
- rewrite H, Zdiv_0_l in H0; elim H0; auto.
- rewrite 2 N_to_Z2P; auto.
- simpl_ndiv; simpl_zdiv; nzsimpl.
- rewrite (Zmult_comm (Z.to_Z z)), <- 2 Zmult_assoc.
- rewrite <- Zgcd_div_swap0; auto with zarith; ring.
+ rewrite Zdiv_gcd_zero in z0; auto with zarith.
+ rewrite H in *. rewrite Zdiv_0_l in *; discriminate.
+ rewrite <- Zmult_assoc, (Zmult_comm (Z.to_Z n)), Zmult_assoc.
+ rewrite Zgcd_div_swap0; try romega.
+ ring.
  Qed.
 
- Lemma strong_spec_mul_norm_Qz_Qq : forall z n d, 
-   Reduced (Qq n d) -> Reduced (mul_norm_Qz_Qq z n d).
+ Instance strong_spec_mul_norm_Qz_Qq z n d :
+   forall `(Reduced (Qq n d)), Reduced (mul_norm_Qz_Qq z n d).
  Proof.
- unfold Reduced; intros z n d.
+ unfold Reduced.
  rewrite 2 strong_spec_red, 2 Qred_iff.
  simpl; nzsimpl.
- destr_neq_bool; intros Hd H; simpl in *; nzsimpl.
- 
+ destr_eqb; intros Hd H; simpl in *; nzsimpl.
+
  unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt.
- destr_zeq_bool; intros Hz; simpl; nzsimpl; simpl; auto.
+ destr_eqb; intros Hz; simpl; nzsimpl; simpl; auto.
  destruct Z_le_gt_dec.
  simpl; nzsimpl.
- destr_neq_bool; simpl; nzsimpl; auto.
- intros H'; elim H'; auto.
- destr_neq_bool; simpl; nzsimpl.
- simpl_ndiv; nzsimpl; rewrite Hd, Zdiv_0_l; intros; discriminate.
+ destr_eqb; simpl; nzsimpl; auto with zarith.
+ unfold norm_denum. destr_eqb; simpl; nzsimpl.
+ rewrite Hd, Zdiv_0_l; discriminate.
  intros _.
- destr_neq_bool; simpl; nzsimpl; auto.
- simpl_ndiv; nzsimpl; rewrite Hd, Zdiv_0_l; intro H'; elim H'; auto.
+ destr_eqb; simpl; nzsimpl; auto.
+ nzsimpl; rewrite Hd, Zdiv_0_l; auto with zarith.
 
- rewrite N_to_Z2P in H; auto.
+ rewrite Z2P_correct in H; auto.
  unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt.
- destr_zeq_bool; intros Hz; simpl; nzsimpl; simpl; auto.
+ destr_eqb; intros Hz; simpl; nzsimpl; simpl; auto.
  destruct Z_le_gt_dec as [H'|H'].
  simpl; nzsimpl.
- destr_neq_bool; simpl; nzsimpl; auto.
+ destr_eqb; simpl; nzsimpl; auto.
  intros.
- rewrite N_to_Z2P; auto.
+ rewrite Z2P_correct; auto.
  apply Zgcd_mult_rel_prime; auto.
   generalize (Zgcd_inv_0_l (Z.to_Z z) (N.to_Z d))
     (Zgcd_is_pos (Z.to_Z z) (N.to_Z d)); romega.
- destr_neq_bool; simpl; nzsimpl; auto.
- simpl_ndiv; simpl_zdiv; nzsimpl.
- intros.
- destr_neq_bool; simpl; nzsimpl; auto.
- simpl_ndiv in *; nzsimpl.
- intros.
- rewrite Z2P_correct.
+ destr_eqb; simpl; nzsimpl; auto.
+ unfold norm_denum.
+ destr_eqb; nzsimpl; simpl; destr_eqb; simpl; auto.
+ intros; nzsimpl.
+ rewrite Z2P_correct; auto.
  apply Zgcd_mult_rel_prime.
  rewrite Zgcd_1_rel_prime.
  apply Zis_gcd_rel_prime.
@@ -652,9 +615,6 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite <- Huv; rewrite Hd0 at 2; ring.
  rewrite Hd0 at 1.
  symmetry; apply Z_div_mult_full; auto with zarith.
- apply Zgcd_div_pos.
- generalize (N.spec_pos d); romega.
- generalize (Zgcd_is_pos (Z.to_Z z) (N.to_Z d)); romega.
  Qed.
 
  Theorem spec_mul_norm : forall x y, [mul_norm x y] == [x] * [y].
@@ -670,37 +630,31 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  destruct (spec_irred ny dx) as (g' & Hg').
  assert (Hz := spec_irred_zero nx dy).
  assert (Hz':= spec_irred_zero ny dx).
- destruct irred as (n1,d1); destruct irred as (n2,d2). 
+ destruct irred as (n1,d1); destruct irred as (n2,d2).
  simpl snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2'].
- rewrite norm_denum.
+ rewrite spec_norm_denum.
  qsimpl.
 
- elim H; destruct (Zmult_integral _ _ H0) as [Eq|Eq].
- rewrite <- Hz' in Eq; rewrite Eq; simpl; auto.
- rewrite <- Hz in Eq; rewrite Eq; nzsimpl; auto.
+ destruct (Zmult_integral _ _ H0) as [Eq|Eq].
+ rewrite Eq in *; simpl in *.
+ rewrite <- Hg2' in *; auto with zarith.
+ rewrite Eq in *; simpl in *.
+ rewrite <- Hg2 in *; auto with zarith.
 
- elim H0; destruct (Zmult_integral _ _ H) as [Eq|Eq].
- rewrite Hz' in Eq; rewrite Eq; simpl; auto.
- rewrite Hz in Eq; rewrite Eq; nzsimpl; auto.
+ destruct (Zmult_integral _ _ H) as [Eq|Eq].
+ rewrite Hz' in Eq; rewrite Eq in *; auto with zarith.
+ rewrite Hz in Eq; rewrite Eq in *; auto with zarith.
 
- rewrite 2 Z2P_correct.
  rewrite <- Hg1, <- Hg2, <- Hg1', <- Hg2'; ring.
-
- assert (0 <= N.to_Z d2 * N.to_Z d1)%Z 
-  by (apply Zmult_le_0_compat; apply N.spec_pos).
- romega.
- assert (0 <= N.to_Z dx * N.to_Z dy)%Z 
-  by (apply Zmult_le_0_compat; apply N.spec_pos).
- romega.
  Qed.
 
- Theorem strong_spec_mul_norm : forall x y,
-  Reduced x -> Reduced y -> Reduced (mul_norm x y).
+ Instance strong_spec_mul_norm x y :
+  forall `(Reduced x, Reduced y), Reduced (mul_norm x y).
  Proof.
  unfold Reduced; intros.
  rewrite strong_spec_red, Qred_iff.
  destruct x as [zx|nx dx]; destruct y as [zy|ny dy].
- simpl in *; auto.
+ simpl in *; auto with zarith.
  simpl.
  rewrite <- Qred_iff, <- strong_spec_red, strong_spec_mul_norm_Qz_Qq; auto.
  simpl.
@@ -712,26 +666,27 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  assert (Hz':= spec_irred_zero ny dx).
  assert (Hgc := strong_spec_irred nx dy).
  assert (Hgc' := strong_spec_irred ny dx).
- destruct irred as (n1,d1); destruct irred as (n2,d2). 
+ destruct irred as (n1,d1); destruct irred as (n2,d2).
  simpl snd in *; destruct Hg as [Hg1 Hg2]; destruct Hg' as [Hg1' Hg2'].
- destr_neq_bool; simpl; nzsimpl; intros.
- apply Zis_gcd_gcd; auto with zarith; apply Zis_gcd_1.
- destr_neq_bool; simpl; nzsimpl; intros.
- auto.
+
+ unfold norm_denum; qsimpl.
+
+ assert (NEQ : N.to_Z dy <> 0%Z) by
+  (rewrite Hz; intros EQ; rewrite EQ in *; romega).
+ specialize (Hgc NEQ).
+
+ assert (NEQ' : N.to_Z dx <> 0%Z) by
+  (rewrite Hz'; intro EQ; rewrite EQ in *; romega).
+ specialize (Hgc' NEQ').
 
  revert H H0.
  rewrite 2 strong_spec_red, 2 Qred_iff; simpl.
- destr_neq_bool; simpl; nzsimpl; intros.
- rewrite Hz in H; rewrite H in H2; nzsimpl; elim H2; auto.
- rewrite Hz' in H0; rewrite H0 in H2; nzsimpl; elim H2; auto.
- rewrite Hz in H; rewrite H in H2; nzsimpl; elim H2; auto.
+ destr_eqb; simpl; nzsimpl; try romega; intros.
+ rewrite Z2P_correct in *; auto.
 
- rewrite N_to_Z2P in *; auto.
- rewrite Z2P_correct.
+ apply Zgcd_mult_rel_prime; rewrite Zgcd_comm;
+  apply Zgcd_mult_rel_prime; rewrite Zgcd_comm; auto.
 
- apply Zgcd_mult_rel_prime; rewrite Zgcd_sym; 
-  apply Zgcd_mult_rel_prime; rewrite Zgcd_sym; auto.
- 
  rewrite Zgcd_1_rel_prime in *.
  apply bezout_rel_prime.
  destruct (rel_prime_bezout _ _ H4) as [u v Huv].
@@ -743,21 +698,17 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  destruct (rel_prime_bezout _ _ H3) as [u v Huv].
  apply Bezout_intro with (u*g)%Z (v*g')%Z.
  rewrite <- Huv, <- Hg2', <- Hg1. ring.
-
- assert (0 <= N.to_Z d2 * N.to_Z d1)%Z.
-  apply Zmult_le_0_compat; apply N.spec_pos.
- romega.
  Qed.
 
- Definition inv (x: t): t := 
+ Definition inv (x: t): t :=
  match x with
- | Qz z => 
-   match Z.compare Z.zero z with 
+ | Qz z =>
+   match Z.compare Z.zero z with
      | Eq => zero
      | Lt => Qq Z.one (Zabs_N z)
      | Gt => Qq Z.minus_one (Zabs_N z)
    end
- | Qq n d => 
+ | Qq n d =>
    match Z.compare Z.zero n with
      | Eq => zero
      | Lt => Qq (Z_of_N d) (Zabs_N n)
@@ -770,13 +721,13 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  destruct x as [ z | n d ].
  (* Qz z *)
  simpl.
- rewrite Zcompare_spec_alt; destr_zcompare.
+ rewrite Z.spec_compare; destr_zcompare.
  (* 0 = z *)
  rewrite <- H.
  simpl; nzsimpl; compute; auto.
  (* 0 < z *)
  simpl.
- destr_neq_bool; nzsimpl; [ intros; rewrite Zabs_eq in *; romega | intros _ ].
+ destr_eqb; nzsimpl; [ intros; rewrite Zabs_eq in *; romega | intros _ ].
  set (z':=Z.to_Z z) in *; clearbody z'.
  red; simpl.
  rewrite Zabs_eq by romega.
@@ -784,7 +735,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  unfold Qinv; simpl; destruct z'; simpl; auto; discriminate.
  (* 0 > z *)
  simpl.
- destr_neq_bool; nzsimpl; [ intros; rewrite Zabs_non_eq in *; romega | intros _ ].
+ destr_eqb; nzsimpl; [ intros; rewrite Zabs_non_eq in *; romega | intros _ ].
  set (z':=Z.to_Z z) in *; clearbody z'.
  red; simpl.
  rewrite Zabs_non_eq by romega.
@@ -792,14 +743,14 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  unfold Qinv; simpl; destruct z'; simpl; auto; discriminate.
  (* Qq n d *)
  simpl.
- rewrite Zcompare_spec_alt; destr_zcompare.
+ rewrite Z.spec_compare; destr_zcompare.
  (* 0 = n *)
  rewrite <- H.
  simpl; nzsimpl.
- destr_neq_bool; intros; compute; auto.
+ destr_eqb; intros; compute; auto.
  (* 0 < n *)
  simpl.
- destr_neq_bool; nzsimpl; intros.
+ destr_eqb; nzsimpl; intros.
  intros; rewrite Zabs_eq in *; romega.
  intros; rewrite Zabs_eq in *; romega.
  clear H1.
@@ -811,10 +762,10 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  red; simpl.
  rewrite Z2P_correct by auto.
  unfold Qinv; simpl; destruct n'; simpl; auto; try discriminate.
- rewrite Zpos_mult_morphism, N_to_Z2P; auto.
+ rewrite Zpos_mult_morphism, Z2P_correct; auto.
  (* 0 > n *)
  simpl.
- destr_neq_bool; nzsimpl; intros.
+ destr_eqb; nzsimpl; intros.
  intros; rewrite Zabs_non_eq in *; romega.
  intros; rewrite Zabs_non_eq in *; romega.
  clear H1.
@@ -826,28 +777,28 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite Z2P_correct by romega.
  unfold Qinv; simpl; destruct n'; simpl; auto; try discriminate.
  assert (T : forall x, Zneg x = Zopp (Zpos x)) by auto.
- rewrite T, Zpos_mult_morphism, N_to_Z2P; auto; ring.
+ rewrite T, Zpos_mult_morphism, Z2P_correct; auto; ring.
  Qed.
 
- Definition inv_norm (x: t): t := 
+ Definition inv_norm (x: t): t :=
    match x with
-     | Qz z => 
-       match Z.compare Z.zero z with 
+     | Qz z =>
+       match Z.compare Z.zero z with
          | Eq => zero
          | Lt => Qq Z.one (Zabs_N z)
          | Gt => Qq Z.minus_one (Zabs_N z)
        end
-     | Qq n d => 
-       if N.eq_bool d N.zero then zero else 
-       match Z.compare Z.zero n with 
+     | Qq n d =>
+       if N.eq_bool d N.zero then zero else
+       match Z.compare Z.zero n with
          | Eq => zero
-         | Lt => 
-           match Z.compare n Z.one with 
+         | Lt =>
+           match Z.compare n Z.one with
              | Gt => Qq (Z_of_N d) (Zabs_N n)
              | _ => Qz (Z_of_N d)
            end
-         | Gt => 
-           match Z.compare n Z.minus_one with 
+         | Gt =>
+           match Z.compare n Z.minus_one with
              | Lt => Qq (Z.opp (Z_of_N d)) (Zabs_N n)
              | _ => Qz (Z.opp (Z_of_N d))
            end
@@ -861,74 +812,72 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  destruct x as [ z | n d ].
  (* Qz z *)
  simpl.
- rewrite Zcompare_spec_alt; destr_zcompare; auto with qarith.
+ rewrite Z.spec_compare; destr_zcompare; auto with qarith.
  (* Qq n d *)
- simpl; nzsimpl; destr_neq_bool.
+ simpl; nzsimpl; destr_eqb.
  destr_zcompare; simpl; auto with qarith.
- destr_neq_bool; nzsimpl; auto with qarith.
+ destr_eqb; nzsimpl; auto with qarith.
  intros _ Hd; rewrite Hd; auto with qarith.
- destr_neq_bool; nzsimpl; auto with qarith.
+ destr_eqb; nzsimpl; auto with qarith.
  intros _ Hd; rewrite Hd; auto with qarith.
  (* 0 < n *)
  destr_zcompare; auto with qarith.
  destr_zcompare; nzsimpl; simpl; auto with qarith; intros.
- destr_neq_bool; nzsimpl; [ intros; rewrite Zabs_eq in *; romega | intros _ ].
+ destr_eqb; nzsimpl; [ intros; rewrite Zabs_eq in *; romega | intros _ ].
  rewrite H0; auto with qarith.
  romega.
  (* 0 > n *)
  destr_zcompare; nzsimpl; simpl; auto with qarith.
- destr_neq_bool; nzsimpl; [ intros; rewrite Zabs_non_eq in *; romega | intros _ ].
+ destr_eqb; nzsimpl; [ intros; rewrite Zabs_non_eq in *; romega | intros _ ].
  rewrite H0; auto with qarith.
  romega.
  Qed.
 
- Theorem strong_spec_inv_norm : forall x, Reduced x -> Reduced (inv_norm x).
+ Instance strong_spec_inv_norm x : Reduced x -> Reduced (inv_norm x).
  Proof.
- unfold Reduced. 
+ unfold Reduced.
  intros.
  destruct x as [ z | n d ].
  (* Qz *)
  simpl; nzsimpl.
  rewrite strong_spec_red, Qred_iff.
  destr_zcompare; simpl; nzsimpl; auto.
- destr_neq_bool; nzsimpl; simpl; auto.
- destr_neq_bool; nzsimpl; simpl; auto.
+ destr_eqb; nzsimpl; simpl; auto.
+ destr_eqb; nzsimpl; simpl; auto.
  (* Qq n d *)
  rewrite strong_spec_red, Qred_iff in H; revert H.
  simpl; nzsimpl.
- destr_neq_bool; nzsimpl; auto with qarith.
+ destr_eqb; nzsimpl; auto with qarith.
  destr_zcompare; simpl; nzsimpl; auto; intros.
  (* 0 < n *)
  destr_zcompare; simpl; nzsimpl; auto.
- destr_neq_bool; nzsimpl; simpl; auto.
+ destr_eqb; nzsimpl; simpl; auto.
  rewrite Zabs_eq; romega.
  intros _.
  rewrite strong_spec_norm; simpl; nzsimpl.
- destr_neq_bool; nzsimpl.
+ destr_eqb; nzsimpl.
  rewrite Zabs_eq; romega.
  intros _.
  rewrite Qred_iff.
  simpl.
  rewrite Zabs_eq; auto with zarith.
- rewrite N_to_Z2P in *; auto.
- rewrite Z2P_correct; auto with zarith.
- rewrite Zgcd_sym; auto.
+ rewrite Z2P_correct in *; auto.
+ rewrite Zgcd_comm; auto.
  (* 0 > n *)
- destr_neq_bool; nzsimpl; simpl; auto; intros.
+ destr_eqb; nzsimpl; simpl; auto; intros.
  destr_zcompare; simpl; nzsimpl; auto.
- destr_neq_bool; nzsimpl.
+ destr_eqb; nzsimpl.
  rewrite Zabs_non_eq; romega.
  intros _.
  rewrite strong_spec_norm; simpl; nzsimpl.
- destr_neq_bool; nzsimpl.
+ destr_eqb; nzsimpl.
  rewrite Zabs_non_eq; romega.
  intros _.
  rewrite Qred_iff.
  simpl.
- rewrite N_to_Z2P in *; auto.
- rewrite Z2P_correct; auto with zarith.
+ rewrite Z2P_correct in *; auto.
  intros.
- rewrite Zgcd_sym, Zgcd_Zabs, Zgcd_sym.
+ rewrite Zgcd_comm, Zgcd_Zabs, Zgcd_comm.
  apply Zis_gcd_gcd; auto with zarith.
  apply Zis_gcd_minus.
  rewrite Zopp_involutive, <- H1; apply Zgcd_is_gcd.
@@ -939,7 +888,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Theorem spec_div x y: [div x y] == [x] / [y].
  Proof.
- intros x y; unfold div; rewrite spec_mul; auto.
+ unfold div; rewrite spec_mul; auto.
  unfold Qdiv; apply Qmult_comp.
  apply Qeq_refl.
  apply spec_inv; auto.
@@ -949,14 +898,14 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Theorem spec_div_norm x y: [div_norm x y] == [x] / [y].
  Proof.
- intros x y; unfold div_norm; rewrite spec_mul_norm; auto.
+ unfold div_norm; rewrite spec_mul_norm; auto.
  unfold Qdiv; apply Qmult_comp.
  apply Qeq_refl.
  apply spec_inv_norm; auto.
  Qed.
- 
- Theorem strong_spec_div_norm : forall x y, 
-   Reduced x -> Reduced y -> Reduced (div_norm x y).
+
+ Instance strong_spec_div_norm x y
+   `(Reduced x, Reduced y) : Reduced (div_norm x y).
  Proof.
  intros; unfold div_norm.
  apply strong_spec_mul_norm; auto.
@@ -974,15 +923,13 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  destruct x as [ z | n d ].
  simpl; rewrite Z.spec_square; red; auto.
  simpl.
- destr_neq_bool; nzsimpl; intros.
+ destr_eqb; nzsimpl; intros.
  apply Qeq_refl.
  rewrite N.spec_square in *; nzsimpl.
- contradict H; elim (Zmult_integral _ _ H0); auto.
+ elim (Zmult_integral _ _ H0); romega.
  rewrite N.spec_square in *; nzsimpl.
- rewrite H in H0; simpl in H0; elim H0; auto.
- assert (0 < N.to_Z d)%Z by (generalize (N.spec_pos d); romega).
- clear H H0.
- rewrite Z.spec_square, N.spec_square.  
+ rewrite H in H0; romega.
+ rewrite Z.spec_square, N.spec_square.
  red; simpl.
  rewrite Zpos_mult_morphism; rewrite !Z2P_correct; auto.
  apply Zmult_lt_0_compat; auto.
@@ -993,7 +940,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
   | Qz zx => Qz (Z.power_pos zx p)
   | Qq nx dx => Qq (Z.power_pos nx p) (N.power_pos dx p)
   end.
- 
+
  Theorem spec_power_pos : forall x p, [power_pos x p] == [x] ^ Zpos p.
  Proof.
  intros [ z | n d ] p; unfold power_pos.
@@ -1006,44 +953,42 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  (* Qq *)
  simpl.
  rewrite Z.spec_power_pos.
- destr_neq_bool; nzsimpl; intros.
+ destr_eqb; nzsimpl; intros.
  apply Qeq_sym; apply Qpower_positive_0.
  rewrite N.spec_power_pos in *.
- assert (0 < N.to_Z d ^ ' p)%Z.
-  apply Zpower_gt_0; auto with zarith.
-  generalize (N.spec_pos d); romega.
+ assert (0 < N.to_Z d ^ ' p)%Z by
+  (apply Zpower_gt_0; auto with zarith).
  romega.
  rewrite N.spec_power_pos, H in *.
- rewrite Zpower_0_l in H0; [ elim H0; auto | discriminate ].
+ rewrite Zpower_0_l in H0; [romega|discriminate].
  rewrite Qpower_decomp.
  red; simpl; do 3 f_equal.
  rewrite Z2P_correct by (generalize (N.spec_pos d); romega).
  rewrite N.spec_power_pos. auto.
  Qed.
 
- Theorem strong_spec_power_pos : forall x p, 
-  Reduced x -> Reduced (power_pos x p).
+ Instance strong_spec_power_pos x p `(Reduced x) : Reduced (power_pos x p).
  Proof.
  destruct x as [z | n d]; simpl; intros.
  red; simpl; auto.
  red; simpl; intros.
  rewrite strong_spec_norm; simpl.
- destr_neq_bool; nzsimpl; intros.
+ destr_eqb; nzsimpl; intros.
  simpl; auto.
  rewrite Qred_iff.
  revert H.
  unfold Reduced; rewrite strong_spec_red, Qred_iff; simpl.
- destr_neq_bool; nzsimpl; simpl; intros.
+ destr_eqb; nzsimpl; simpl; intros.
  rewrite N.spec_power_pos in H0.
- elim H0; rewrite H; rewrite Zpower_0_l; auto; discriminate.
- rewrite N_to_Z2P in *; auto.
+ rewrite H, Zpower_0_l in *; [romega|discriminate].
+ rewrite Z2P_correct in *; auto.
  rewrite N.spec_power_pos, Z.spec_power_pos; auto.
  rewrite Zgcd_1_rel_prime in *.
  apply rel_prime_Zpower; auto with zarith.
  Qed.
 
- Definition power (x : t) (z : Z) : t := 
-   match z with 
+ Definition power (x : t) (z : Z) : t :=
+   match z with
      | Z0 => one
      | Zpos p => power_pos x p
      | Zneg p => inv (power_pos x p)
@@ -1058,8 +1003,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite spec_inv, spec_power_pos; apply Qeq_refl.
  Qed.
 
- Definition power_norm (x : t) (z : Z) : t := 
-   match z with 
+ Definition power_norm (x : t) (z : Z) : t :=
+   match z with
      | Z0 => one
      | Zpos p => power_pos x p
      | Zneg p => inv_norm (power_pos x p)
@@ -1074,7 +1019,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite spec_inv_norm, spec_power_pos; apply Qeq_refl.
  Qed.
 
- Theorem strong_spec_power_norm : forall x z, 
+ Instance strong_spec_power_norm x z :
    Reduced x -> Reduced (power_norm x z).
  Proof.
  destruct z; simpl.
@@ -1087,7 +1032,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
 
  (** Interaction with [Qcanon.Qc] *)
- 
+
  Open Scope Qc_scope.
 
  Definition of_Qc q := of_Q (this q).
@@ -1102,7 +1047,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  unfold of_Qc; rewrite strong_spec_of_Q; auto.
  Qed.
 
- Lemma strong_spec_of_Qc_bis : forall q, Reduced (of_Qc q).
+ Instance strong_spec_of_Qc_bis q : Reduced (of_Qc q).
  Proof.
  intros; red; rewrite strong_spec_red, strong_spec_of_Qc.
  destruct q; simpl; auto.
@@ -1143,7 +1088,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_addc x y:
   [[add x y]] = [[x]] + [[y]].
  Proof.
- intros x y; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! ([x] + [y])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
@@ -1157,7 +1102,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_add_normc x y:
   [[add_norm x y]] = [[x]] + [[y]].
  Proof.
- intros x y; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! ([x] + [y])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
@@ -1168,7 +1113,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  apply Qplus_comp; apply Qeq_sym; apply Qred_correct.
  Qed.
 
- Theorem spec_add_normc_bis : forall x y : Qc, 
+ Theorem spec_add_normc_bis : forall x y : Qc,
    [add_norm (of_Qc x) (of_Qc y)] = x+y.
  Proof.
  intros.
@@ -1180,18 +1125,18 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Theorem spec_subc x y:  [[sub x y]] = [[x]] - [[y]].
  Proof.
- intros x y; unfold sub; rewrite spec_addc; auto.
+ unfold sub; rewrite spec_addc; auto.
  rewrite spec_oppc; ring.
  Qed.
 
  Theorem spec_sub_normc x y:
    [[sub_norm x y]] = [[x]] - [[y]].
  Proof.
- intros x y; unfold sub_norm; rewrite spec_add_normc; auto.
+ unfold sub_norm; rewrite spec_add_normc; auto.
  rewrite spec_oppc; ring.
  Qed.
 
- Theorem spec_sub_normc_bis : forall x y : Qc, 
+ Theorem spec_sub_normc_bis : forall x y : Qc,
    [sub_norm (of_Qc x) (of_Qc y)] = x-y.
  Proof.
  intros.
@@ -1199,13 +1144,13 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite strong_spec_red.
  symmetry; apply (Qred_complete (x+(-y)%Qc)%Q).
  rewrite spec_sub_norm, ! strong_spec_of_Qc.
- unfold Qcopp, Q2Qc; rewrite Qred_correct; auto with qarith.
+ unfold Qcopp, Q2Qc, this. rewrite Qred_correct ; auto with qarith.
  Qed.
 
  Theorem spec_mulc x y:
   [[mul x y]] = [[x]] * [[y]].
  Proof.
- intros x y; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! ([x] * [y])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
@@ -1219,7 +1164,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_mul_normc x y:
    [[mul_norm x y]] = [[x]] * [[y]].
  Proof.
- intros x y; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! ([x] * [y])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
@@ -1230,7 +1175,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  apply Qmult_comp; apply Qeq_sym; apply Qred_correct.
  Qed.
 
- Theorem spec_mul_normc_bis : forall x y : Qc, 
+ Theorem spec_mul_normc_bis : forall x y : Qc,
    [mul_norm (of_Qc x) (of_Qc y)] = x*y.
  Proof.
  intros.
@@ -1243,7 +1188,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_invc x:
    [[inv x]] =  /[[x]].
  Proof.
- intros x; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! (/[x])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
@@ -1257,7 +1202,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_inv_normc x:
    [[inv_norm x]] =  /[[x]].
  Proof.
- intros x; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! (/[x])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
@@ -1268,7 +1213,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  apply Qinv_comp; apply Qeq_sym; apply Qred_correct.
  Qed.
 
- Theorem spec_inv_normc_bis : forall x : Qc, 
+ Theorem spec_inv_normc_bis : forall x : Qc,
    [inv_norm (of_Qc x)] = /x.
  Proof.
  intros.
@@ -1280,19 +1225,19 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Theorem spec_divc x y: [[div x y]] = [[x]] / [[y]].
  Proof.
- intros x y; unfold div; rewrite spec_mulc; auto.
+ unfold div; rewrite spec_mulc; auto.
  unfold Qcdiv; apply f_equal2 with (f := Qcmult); auto.
- apply spec_invc; auto. 
+ apply spec_invc; auto.
  Qed.
 
  Theorem spec_div_normc x y: [[div_norm x y]] = [[x]] / [[y]].
  Proof.
- intros x y; unfold div_norm; rewrite spec_mul_normc; auto.
+ unfold div_norm; rewrite spec_mul_normc; auto.
  unfold Qcdiv; apply f_equal2 with (f := Qcmult); auto.
  apply spec_inv_normc; auto.
  Qed.
 
- Theorem spec_div_normc_bis : forall x y : Qc, 
+ Theorem spec_div_normc_bis : forall x y : Qc,
    [div_norm (of_Qc x) (of_Qc y)] = x/y.
  Proof.
  intros.
@@ -1300,12 +1245,12 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite strong_spec_red.
  symmetry; apply (Qred_complete (x*(/y)%Qc)%Q).
  rewrite spec_div_norm, ! strong_spec_of_Qc.
- unfold Qcinv, Q2Qc; rewrite Qred_correct; auto with qarith.
+ unfold Qcinv, Q2Qc, this; rewrite Qred_correct; auto with qarith.
  Qed.
 
- Theorem spec_squarec x: [[square x]] =  [[x]]^2.
+ Theorem spec_squarec x: [[square x]] = [[x]]^2.
  Proof.
- intros x; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! ([x]^2)).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
@@ -1322,7 +1267,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_power_posc x p:
    [[power_pos x p]] = [[x]] ^ nat_of_P p.
  Proof.
- intros x p; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! ([x]^Zpos p)).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
diff --git a/theories/Numbers/Rational/SpecViaQ/QSig.v b/theories/Numbers/Rational/SpecViaQ/QSig.v
index be9b2d4e..10d0189a 100644
--- a/theories/Numbers/Rational/SpecViaQ/QSig.v
+++ b/theories/Numbers/Rational/SpecViaQ/QSig.v
@@ -6,9 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: QSig.v 11207 2008-07-04 16:50:32Z letouzey $ i*)
+(*i $Id$ i*)
 
-Require Import QArith Qpower.
+Require Import QArith Qpower Qminmax Orders RelationPairs GenericMinMax.
 
 Open Scope Q_scope.
 
@@ -23,75 +23,203 @@ Module Type QType.
  Parameter t : Type.
 
  Parameter to_Q : t -> Q.
- Notation "[ x ]" := (to_Q x).
+ Local Notation "[ x ]" := (to_Q x).
 
  Definition eq x y := [x] == [y].
+ Definition lt x y := [x] < [y].
+ Definition le x y := [x] <= [y].
 
  Parameter of_Q : Q -> t.
  Parameter spec_of_Q: forall x, to_Q (of_Q x) == x.
 
+ Parameter red : t -> t.
+ Parameter compare : t -> t -> comparison.
+ Parameter eq_bool : t -> t -> bool.
+ Parameter max : t -> t -> t.
+ Parameter min : t -> t -> t.
  Parameter zero : t.
  Parameter one : t.
  Parameter minus_one : t.
+ Parameter add : t -> t -> t.
+ Parameter sub : t -> t -> t.
+ Parameter opp : t -> t.
+ Parameter mul : t -> t -> t.
+ Parameter square : t -> t.
+ Parameter inv : t -> t.
+ Parameter div : t -> t -> t.
+ Parameter power : t -> Z -> t.
 
+ Parameter spec_red : forall x, [red x] == [x].
+ Parameter strong_spec_red : forall x, [red x] = Qred [x].
+ Parameter spec_compare : forall x y, compare x y = ([x] ?= [y]).
+ Parameter spec_eq_bool : forall x y, eq_bool x y = Qeq_bool [x] [y].
+ Parameter spec_max : forall x y, [max x y] == Qmax [x] [y].
+ Parameter spec_min : forall x y, [min x y] == Qmin [x] [y].
  Parameter spec_0: [zero] == 0.
  Parameter spec_1: [one] == 1.
  Parameter spec_m1: [minus_one] == -(1).
+ Parameter spec_add: forall x y, [add x y] == [x] + [y].
+ Parameter spec_sub: forall x y, [sub x y] == [x] - [y].
+ Parameter spec_opp: forall x, [opp x] == - [x].
+ Parameter spec_mul: forall x y, [mul x y] == [x] * [y].
+ Parameter spec_square: forall x, [square x] == [x] ^ 2.
+ Parameter spec_inv : forall x, [inv x] == / [x].
+ Parameter spec_div: forall x y, [div x y] == [x] / [y].
+ Parameter spec_power: forall x z, [power x z] == [x] ^ z.
 
- Parameter compare : t -> t -> comparison.
+End QType.
 
- Parameter spec_compare : forall x y, compare x y = ([x] ?= [y]).
+(** NB: several of the above functions come with [..._norm] variants
+     that expect reduced arguments and return reduced results. *)
 
- Definition lt n m := compare n m = Lt.
- Definition le n m := compare n m <> Gt.
- Definition min n m := match compare n m with Gt => m | _ => n end.
- Definition max n m := match compare n m with Lt => m | _ => n end.
+(** TODO : also speak of specifications via Qcanon ... *)
 
- Parameter eq_bool : t -> t -> bool.
- 
- Parameter spec_eq_bool : forall x y, 
-  if eq_bool x y then [x]==[y] else ~([x]==[y]).
+Module Type QType_Notation (Import Q : QType).
+ Notation "[ x ]" := (to_Q x).
+ Infix "=="  := eq (at level 70).
+ Notation "x != y" := (~x==y) (at level 70).
+ Infix "<=" := le.
+ Infix "<" := lt.
+ Notation "0" := zero.
+ Notation "1" := one.
+ Infix "+" := add.
+ Infix "-" := sub.
+ Infix "*" := mul.
+ Notation "- x" := (opp x).
+ Infix "/" := div.
+ Notation "/ x" := (inv x).
+ Infix "^" := power.
+End QType_Notation.
 
- Parameter red : t -> t.
- 
- Parameter spec_red : forall x, [red x] == [x].
- Parameter strong_spec_red : forall x, [red x] = Qred [x].
+Module Type QType' := QType <+ QType_Notation.
 
- Parameter add : t -> t -> t.
 
- Parameter spec_add: forall x y, [add x y] == [x] + [y].
+Module QProperties (Import Q : QType').
 
- Parameter sub : t -> t -> t.
+(** Conversion to Q *)
 
- Parameter spec_sub: forall x y, [sub x y] == [x] - [y].
+Hint Rewrite
+ spec_red spec_compare spec_eq_bool spec_min spec_max
+ spec_add spec_sub spec_opp spec_mul spec_square spec_inv spec_div
+ spec_power : qsimpl.
+Ltac qify := unfold eq, lt, le in *; autorewrite with qsimpl;
+ try rewrite spec_0 in *; try rewrite spec_1 in *; try rewrite spec_m1 in *.
 
- Parameter opp : t -> t.
+(** NB: do not add [spec_0] in the autorewrite database. Otherwise,
+    after instanciation in BigQ, this lemma become convertible to 0=0,
+    and autorewrite loops. Idem for [spec_1] and [spec_m1] *)
 
- Parameter spec_opp: forall x, [opp x] == - [x].
+(** Morphisms *)
 
- Parameter mul : t -> t -> t.
+Ltac solve_wd1 := intros x x' Hx; qify; now rewrite Hx.
+Ltac solve_wd2 := intros x x' Hx y y' Hy; qify; now rewrite Hx, Hy.
 
- Parameter spec_mul: forall x y, [mul x y] == [x] * [y].
+Local Obligation Tactic := solve_wd2 || solve_wd1.
 
- Parameter square : t -> t.
+Instance : Measure to_Q.
+Instance eq_equiv : Equivalence eq.
 
- Parameter spec_square: forall x, [square x] == [x] ^ 2.
+Program Instance lt_wd : Proper (eq==>eq==>iff) lt.
+Program Instance le_wd : Proper (eq==>eq==>iff) le.
+Program Instance red_wd : Proper (eq==>eq) red.
+Program Instance compare_wd : Proper (eq==>eq==>Logic.eq) compare.
+Program Instance eq_bool_wd : Proper (eq==>eq==>Logic.eq) eq_bool.
+Program Instance min_wd : Proper (eq==>eq==>eq) min.
+Program Instance max_wd : Proper (eq==>eq==>eq) max.
+Program Instance add_wd : Proper (eq==>eq==>eq) add.
+Program Instance sub_wd : Proper (eq==>eq==>eq) sub.
+Program Instance opp_wd : Proper (eq==>eq) opp.
+Program Instance mul_wd : Proper (eq==>eq==>eq) mul.
+Program Instance square_wd : Proper (eq==>eq) square.
+Program Instance inv_wd : Proper (eq==>eq) inv.
+Program Instance div_wd : Proper (eq==>eq==>eq) div.
+Program Instance power_wd : Proper (eq==>Logic.eq==>eq) power.
 
- Parameter inv : t -> t.
+(** Let's implement [HasCompare] *)
 
- Parameter spec_inv : forall x, [inv x] == / [x].
+Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+Proof. intros. qify. destruct (Qcompare_spec [x] [y]); auto. Qed.
 
- Parameter div : t -> t -> t.
+(** Let's implement [TotalOrder] *)
 
- Parameter spec_div: forall x y, [div x y] == [x] / [y].
+Definition lt_compat := lt_wd.
+Instance lt_strorder : StrictOrder lt.
 
- Parameter power : t -> Z -> t.
+Lemma le_lteq : forall x y, x<=y <-> x<y \/ x==y.
+Proof. intros. qify. apply Qle_lteq. Qed.
 
- Parameter spec_power: forall x z, [power x z] == [x] ^ z.
+Lemma lt_total : forall x y, x<y \/ x==y \/ y<x.
+Proof. intros. destruct (compare_spec x y); auto. Qed.
 
-End QType.
+(** Let's implement [HasEqBool] *)
 
-(** NB: several of the above functions come with [..._norm] variants
-     that expect reduced arguments and return reduced results. *)
+Definition eqb := eq_bool.
 
-(** TODO : also speak of specifications via Qcanon ... *)
+Lemma eqb_eq : forall x y, eq_bool x y = true <-> x == y.
+Proof. intros. qify. apply Qeq_bool_iff. Qed.
+
+Lemma eqb_correct : forall x y, eq_bool x y = true -> x == y.
+Proof. now apply eqb_eq. Qed.
+
+Lemma eqb_complete : forall x y, x == y -> eq_bool x y = true.
+Proof. now apply eqb_eq. Qed.
+
+(** Let's implement [HasMinMax] *)
+
+Lemma max_l : forall x y, y<=x -> max x y == x.
+Proof. intros x y. qify. apply Qminmax.Q.max_l. Qed.
+
+Lemma max_r : forall x y, x<=y -> max x y == y.
+Proof. intros x y. qify. apply Qminmax.Q.max_r. Qed.
+
+Lemma min_l : forall x y, x<=y -> min x y == x.
+Proof. intros x y. qify. apply Qminmax.Q.min_l. Qed.
+
+Lemma min_r : forall x y, y<=x -> min x y == y.
+Proof. intros x y. qify. apply Qminmax.Q.min_r. Qed.
+
+(** Q is a ring *)
+
+Lemma add_0_l : forall x, 0+x == x.
+Proof. intros. qify. apply Qplus_0_l. Qed.
+
+Lemma add_comm : forall x y, x+y == y+x.
+Proof. intros. qify. apply Qplus_comm. Qed.
+
+Lemma add_assoc : forall x y z, x+(y+z) == x+y+z.
+Proof. intros. qify. apply Qplus_assoc. Qed.
+
+Lemma mul_1_l : forall x, 1*x == x.
+Proof. intros. qify. apply Qmult_1_l. Qed.
+
+Lemma mul_comm : forall x y, x*y == y*x.
+Proof. intros. qify. apply Qmult_comm. Qed.
+
+Lemma mul_assoc : forall x y z, x*(y*z) == x*y*z.
+Proof. intros. qify. apply Qmult_assoc. Qed.
+
+Lemma mul_add_distr_r : forall x y z, (x+y)*z == x*z + y*z.
+Proof. intros. qify. apply Qmult_plus_distr_l. Qed.
+
+Lemma sub_add_opp : forall x y, x-y == x+(-y).
+Proof. intros. qify. now unfold Qminus. Qed.
+
+Lemma add_opp_diag_r : forall x, x+(-x) == 0.
+Proof. intros. qify. apply Qplus_opp_r. Qed.
+
+(** Q is a field *)
+
+Lemma neq_1_0 : 1!=0.
+Proof. intros. qify. apply Q_apart_0_1. Qed.
+
+Lemma div_mul_inv : forall x y, x/y == x*(/y).
+Proof. intros. qify. now unfold Qdiv. Qed.
+
+Lemma mul_inv_diag_l : forall x, x!=0 -> /x * x == 1.
+Proof. intros x. qify. rewrite Qmult_comm. apply Qmult_inv_r. Qed.
+
+End QProperties.
+
+Module QTypeExt (Q : QType)
+ <: QType <: TotalOrder <: HasCompare Q <: HasMinMax Q <: HasEqBool Q
+ := Q <+ QProperties.
\ No newline at end of file