- transcript: bugfix

[helm.git] / helm / software / matita / library / Q / inv.ma

diff --git a/helm/software/matita/library/Q/inv.ma b/helm/software/matita/library/Q/inv.ma
index 9cc2fc3b43ea9c7c06fd001338221d0c38d37759..4cc38f191a47a1735045b289bf2f4d10d49d26f1 100644 (file)
--- 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