X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2Finv.ma;h=4cc38f191a47a1735045b289bf2f4d10d49d26f1;hb=3cf6181bded05eb63140d1b2ba4f2f5791a73b48;hp=9cc2fc3b43ea9c7c06fd001338221d0c38d37759;hpb=ca41435a6021292ccba239aa173651c0be705b45;p=helm.git

diff --git a/helm/software/matita/library/Q/inv.ma b/helm/software/matita/library/Q/inv.ma
index 9cc2fc3b4..4cc38f191 100644
--- a/helm/software/matita/library/Q/inv.ma
+++ b/helm/software/matita/library/Q/inv.ma
@@ -12,9 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "Q/q/q.ma".
 include "Q/q.ma".
+include "Q/fraction/finv.ma".
 
-alias id "finv" = "cic:/matita/Q/fraction/finv/finv.con".
 theorem denominator_integral_factor_finv:
  ∀f. enumerator_integral_fraction f = denominator_integral_fraction (finv f).
  intro;
@@ -25,7 +26,6 @@ theorem denominator_integral_factor_finv:
    elim z; simplify; reflexivity]
 qed.
 
-alias id "Qpos" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1/2)".
 definition is_positive ≝
  λq.
   match q with
@@ -33,7 +33,6 @@ definition is_positive ≝
    | _ ⇒ False
    ].
 
-alias id "Qneg" = "cic:/matita/Q/q/q/Q.ind#xpointer(1/1/3)".
 definition is_negative ≝
  λq.
   match q with