X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2Ffrac.ma;h=863efe2833be3770cc257551e5863de628d6566f;hb=dcef667a444aa0f189225855c1433d26b65fb8b7;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..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
@@ -52,8 +54,6 @@ reflexivity.
 qed.
 *)
 
-Qtimes1 == Qtimes_numerator_denominator
-
 (*     
 definition numQ:Q \to Z \def
 \lambda q. 
@@ -83,7 +83,7 @@ elim r
   |elim f
     [reflexivity
     |reflexivity
-    |apply Qtimes1.
+    |apply Qtimes_numerator_denominator.
     ]
   ]
 qed.*)
@@ -101,7 +101,7 @@ elim r
   |elim f
     [reflexivity
     |reflexivity
-    |apply Qtimes1.
+    |apply Qtimes_numerator_denominator.
     ]
   ]
 qed.*)