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

diff --git a/helm/software/matita/library/Q/frac.ma b/helm/software/matita/library/Q/frac.ma
index a1f0cd54a..9ce493604 100644
--- a/helm/software/matita/library/Q/frac.ma
+++ b/helm/software/matita/library/Q/frac.ma
@@ -52,8 +52,6 @@ reflexivity.
 qed.
 *)
 
-Qtimes1 == Qtimes_numerator_denominator
-
 (*     
 definition numQ:Q \to Z \def
 \lambda q. 
@@ -64,9 +62,14 @@ 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)).
 
@@ -83,7 +86,7 @@ elim r
   |elim f
     [reflexivity
     |reflexivity
-    |apply Qtimes1.
+    |apply Qtimes_numerator_denominator.
     ]
   ]
 qed.*)
@@ -101,11 +104,13 @@ elim r
   |elim f
     [reflexivity
     |reflexivity
-    |apply Qtimes1.
+    |apply Qtimes_numerator_denominator.
     ]
   ]
 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