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

diff --git a/helm/software/matita/library/Q/inv.ma b/helm/software/matita/library/Q/inv.ma
index 39b9c776e..9cc2fc3b4 100644
--- a/helm/software/matita/library/Q/inv.ma
+++ b/helm/software/matita/library/Q/inv.ma
@@ -14,55 +14,7 @@
 
 include "Q/q.ma".
 
-let rec finv f \def
-  match f with
-  [ (pp n) \Rightarrow (nn n)
-  | (nn n) \Rightarrow (pp n)
-  | (cons x g) \Rightarrow (cons (Zopp x) (finv g))].
-
-theorem finv_finv: ∀f. finv (finv f) = f.
- intro;
- elim f;
-  [1,2: reflexivity
-  | simplify;
-    rewrite > H;
-    rewrite > Zopp_Zopp;
-    reflexivity
-  ]
-qed.
-
-definition rinv : ratio \to ratio \def
-\lambda r:ratio.
-  match r with
-  [one \Rightarrow one
-  | (frac f) \Rightarrow frac (finv f)].
-
-theorem rinv_rinv: ∀r. rinv (rinv r) = r.
- intro;
- elim r;
-  [ reflexivity
-  | simplify;
-    rewrite > finv_finv;
-    reflexivity]
-qed.
-
-definition Qinv : Q → Q ≝
- λp.
-  match p with
-   [ OQ ⇒ OQ  (* arbitrary value *)
-   | Qpos r ⇒ Qpos (rinv r)
-   | Qneg r ⇒ Qneg (rinv r)
-   ].
-
-theorem Qinv_Qinv: ∀q. Qinv (Qinv q) = q.
- intro;
- elim q;
-  [ reflexivity
-  |*:simplify;
-    rewrite > rinv_rinv;
-    reflexivity]
-qed.
-
+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;
@@ -73,6 +25,7 @@ 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
@@ -80,6 +33,7 @@ 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
@@ -87,6 +41,7 @@ definition is_negative ≝
    | _ ⇒ False
    ].
 
+(*
 theorem is_positive_denominator_Qinv:
  ∀q. is_positive q → enumerator q = denominator (Qinv q).
  intro;
@@ -125,7 +80,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:
@@ -134,5 +89,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]
-qed.
\ No newline at end of file
+  | elim q in H ⊢ %; assumption]
+qed.
+*)
\ No newline at end of file