(* *)
(**************************************************************************)
+include "Q/q/qinv.ma".
+
(*
let rec nat_fact_to_fraction_inv l \def
match l with
].
*)
-alias id "numeratorQ" = "cic:/matita/Q/q/q/numeratorQ.con".
-alias id "nat" = "cic:/matita/nat/nat/nat.ind#xpointer(1/1)".
-alias id "defactorize" = "cic:/matita/nat/factorization/defactorize.con".
-alias id "Q" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1)".
definition numQ:Q \to nat \def
\lambda q. defactorize (numeratorQ q).
-alias id "Qinv" = "cic:/matita/Q/q/qinv/Qinv.con".
definition denomQ:Q \to nat \def
\lambda q. defactorize (numeratorQ (Qinv q)).
]
qed.*)
-alias id "Qpos" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1/2)".
-alias id "OQ" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1/1)".
definition Qabs:Q \to Q \def \lambda q.
match q with
[OQ \Rightarrow OQ