Even more Q stuff moved around.

[helm.git] / helm / software / matita / library / Q / fraction / finv.ma

diff --git a/helm/software/matita/library/Q/fraction/finv.ma b/helm/software/matita/library/Q/fraction/finv.ma
index 2868bece0cd85f4d48217abbc0b3b16342cc68d1..ce05b29c7132bae42df04bfd77e196f13890f4aa 100644 (file)
--- a/helm/software/matita/library/Q/fraction/finv.ma
+++ b/helm/software/matita/library/Q/fraction/finv.ma
@@ -15,11 +15,11 @@
 include "Z/plus.ma".
 include "Q/fraction/fraction.ma".
 
-let rec finv f \def                                               
+let rec finv f ≝                                               
   match f with
-  [ (pp n) \Rightarrow (nn n)
-  | (nn n) \Rightarrow (pp n)
-  | (cons x g) \Rightarrow (cons (Zopp x) (finv g))].
+  [ pp n ⇒ nn n
+  | nn n ⇒ pp n
+  | cons x g ⇒ cons (Zopp x) (finv g)].
 
 theorem finv_finv: ∀f. finv (finv f) = f.
  intro; 
@@ -31,62 +31,3 @@ theorem finv_finv: ∀f. finv (finv f) = f.
     reflexivity
   ]
 qed.
-
-theorem or_numerator_nfa_one_nfa_proper: 
-∀f.
- (numerator f = nfa_one ∧ ∃g.numerator (finv f) = nfa_proper g) ∨
- ∃g.numerator f = nfa_proper g.
-intro.elim f
-  [simplify.right.
-   apply (ex_intro ? ? (nf_last n)).reflexivity
-  |simplify.left.split
-    [reflexivity
-    |apply (ex_intro ? ? (nf_last n)).reflexivity
-    ]
-  |elim H;clear H
-    [elim H1.clear H1.
-     elim H2.clear H2.
-     elim z
-      [simplify.
-       rewrite > H.rewrite > H1.simplify.
-       left.split
-        [reflexivity
-        |apply (ex_intro ? ? (nf_cons O a)).reflexivity
-        ]
-      |simplify.
-       rewrite > H.rewrite > H1.simplify.
-       right.apply (ex_intro ? ? (nf_last n)).reflexivity
-      |simplify.
-       rewrite > H.rewrite > H1.simplify.
-       left.split
-        [reflexivity
-        |apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
-        ]
-      ]
-    |elim H1.clear H1.
-      elim z
-      [simplify.
-       rewrite > H.simplify.
-       right.
-       apply (ex_intro ? ? (nf_cons O a)).reflexivity
-      |simplify.
-       rewrite > H.simplify.
-       right.apply (ex_intro ? ? (nf_cons (S n) a)).reflexivity
-      |simplify.
-       rewrite > H.simplify.
-       right.
-       apply (ex_intro ? ? (nf_cons O a)).reflexivity
-      ]
-    ]
-  ]
-qed.
-  
-theorem eq_nfa_one_to_eq_finv_nfa_proper: 
-∀f.numerator f = nfa_one → ∃h.numerator (finv f) = nfa_proper h.
-  intros;
-  elim (or_numerator_nfa_one_nfa_proper f); cases H1;
-   [ assumption
-   | rewrite > H in H2;
-     destruct
-   ]
-qed.