1 files changed, 22 insertions, 44 deletions

diff --git a/theories/Numbers/Rational/SpecViaQ/QSig.v b/theories/Numbers/Rational/SpecViaQ/QSig.v
index 8be66493e5..1959f4ad69 100644
--- a/theories/Numbers/Rational/SpecViaQ/QSig.v
+++ b/theories/Numbers/Rational/SpecViaQ/QSig.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import QArith Qpower.
+Require Import QArith Qpower Qminmax.
 
 Open Scope Q_scope.
 
@@ -26,67 +26,45 @@ Module Type QType.
  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 compare : t -> t -> comparison.
-
- Parameter spec_compare : forall x y, compare x y = ([x] ?= [y]).
-
- 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.
-
- Parameter eq_bool : t -> t -> bool.
-
- Parameter spec_eq_bool : forall x y,
-  if eq_bool x y then [x]==[y] else ~([x]==[y]).
-
- Parameter red : t -> t.
-
- Parameter spec_red : forall x, [red x] == [x].
- Parameter strong_spec_red : forall x, [red x] = Qred [x].
-
- Parameter add : t -> t -> t.
-
  Parameter spec_add: forall x y, [add x y] == [x] + [y].
-
- Parameter sub : t -> t -> t.
-
  Parameter spec_sub: forall x y, [sub x y] == [x] - [y].
-
- Parameter opp : t -> t.
-
  Parameter spec_opp: forall x, [opp x] == - [x].
-
- Parameter mul : t -> t -> t.
-
  Parameter spec_mul: forall x y, [mul x y] == [x] * [y].
-
- Parameter square : t -> t.
-
  Parameter spec_square: forall x, [square x] == [x] ^ 2.
-
- Parameter inv : t -> t.
-
  Parameter spec_inv : forall x, [inv x] == / [x].
-
- Parameter div : t -> t -> t.
-
  Parameter spec_div: forall x y, [div x y] == [x] / [y].
-
- Parameter power : t -> Z -> t.
-
  Parameter spec_power: forall x z, [power x z] == [x] ^ z.
 
 End QType.