better notation for oalgebra

[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 39b9c776e9ae997ab4cafe70c147094392e73797..4cc38f191a47a1735045b289bf2f4d10d49d26f1 100644 (file)
--- a/helm/software/matita/library/Q/inv.ma
+++ b/helm/software/matita/library/Q/inv.ma
@@ -12,56 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "Q/q/q.ma".
 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.
+include "Q/fraction/finv.ma".
 
 theorem denominator_integral_factor_finv:
  ∀f. enumerator_integral_fraction f = denominator_integral_fraction (finv f).
@@ -87,6 +40,7 @@ definition is_negative ≝
    | _ ⇒ False
    ].
 
+(*
 theorem is_positive_denominator_Qinv:
  ∀q. is_positive q → enumerator q = denominator (Qinv q).
  intro;
@@ -125,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:
@@ -134,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]
-qed.
\ No newline at end of file
+  | elim q in H ⊢ %; assumption]
+qed.
+*)
\ No newline at end of file