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=8c6f1db95ecffd4d98e08768f28fc04564a1c92e;hpb=13ee180b4b982b7a150e8d727ed4b83813ac3fa2;p=helm.git

diff --git a/helm/software/matita/library/Q/inv.ma b/helm/software/matita/library/Q/inv.ma
index 8c6f1db95..4cc38f191 100644
--- a/helm/software/matita/library/Q/inv.ma
+++ b/helm/software/matita/library/Q/inv.ma
@@ -12,7 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "Q/q/q.ma".
 include "Q/q.ma".
+include "Q/fraction/finv.ma".
 
 theorem denominator_integral_factor_finv:
  ∀f. enumerator_integral_fraction f = denominator_integral_fraction (finv f).
@@ -38,6 +40,7 @@ definition is_negative ≝
    | _ ⇒ False
    ].
 
+(*
 theorem is_positive_denominator_Qinv:
  ∀q. is_positive q → enumerator q = denominator (Qinv q).
  intro;
@@ -76,7 +79,7 @@ theorem is_positive_enumerator_Qinv:
  lapply (is_positive_denominator_Qinv (Qinv q));
   [ rewrite > Qinv_Qinv in Hletin;
     assumption
-  | generalize in match H; elim q; assumption]
+  | elim q in H ⊢ %; assumption]
 qed.
 
 theorem is_negative_enumerator_Qinv:
@@ -85,5 +88,6 @@ theorem is_negative_enumerator_Qinv:
  lapply (is_negative_denominator_Qinv (Qinv q));
   [ rewrite > Qinv_Qinv in Hletin;
     assumption
-  | generalize in match H; elim q; assumption]
+  | elim q in H ⊢ %; assumption]
 qed.
+*)
\ No newline at end of file