X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2Ffrac.ma;h=863efe2833be3770cc257551e5863de628d6566f;hb=a88be1ca42c0969dbab9a5c76240f5931df876d9;hp=9ce49360496d4e3b02d641effccacbc9e6833deb;hpb=ca41435a6021292ccba239aa173651c0be705b45;p=helm.git

diff --git a/helm/software/matita/library/Q/frac.ma b/helm/software/matita/library/Q/frac.ma
index 9ce493604..863efe283 100644
--- a/helm/software/matita/library/Q/frac.ma
+++ b/helm/software/matita/library/Q/frac.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "Q/q/qinv.ma".
+
 (*
 let rec nat_fact_to_fraction_inv l \def
   match l with
@@ -62,14 +64,9 @@ match q 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)).
 
@@ -109,8 +106,6 @@ elim r
   ]
 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