(**************************************************************************)
include "Q/ratio/ratio.ma".
+include "Q/fraction/numerator_denominator.ma".
(* a rational number is either O or a ratio with a sign *)
inductive Q : Set \def
| Qpos : ratio \to Q
| Qneg : ratio \to Q.
+interpretation "Rationals" 'Q = Q.
+
definition Qone ≝ Qpos one.
definition Qopp ≝