X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2Ffrac.ma;h=863efe2833be3770cc257551e5863de628d6566f;hb=277fc8ff21ce3dbd6893b1994c55cf5c06a98355;hp=d00cd3158956c72f9f59e3a479a9b7850eebfa79;hpb=7a116453d799657958e32693be28d18a5aab84fc;p=helm.git

diff --git a/helm/software/matita/library/Q/frac.ma b/helm/software/matita/library/Q/frac.ma
index d00cd3158..863efe283 100644
--- a/helm/software/matita/library/Q/frac.ma
+++ b/helm/software/matita/library/Q/frac.ma
@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "Q/q/qinv.ma".
+
 (*
 let rec nat_fact_to_fraction_inv l \def
   match l with
@@ -52,112 +54,6 @@ reflexivity.
 qed.
 *)
 
-(* la prova seguente e' tutta una ripetizione. Sistemare. *)
-(*CSC
-theorem Qtimes1: \forall f:fraction.
-Qtimes (nat_fact_all_to_Q (numerator f))
-(Qinv (nat_fact_all_to_Q (numerator (finv f))))
-= Qpos (frac f).
-simplify.
-intro.elim f
-  [reflexivity
-  |reflexivity
-  |elim (or_numerator_nfa_one_nfa_proper f1)
-    [elim H1.clear H1.
-     elim H3.clear H3.
-     cut (finv (nat_fact_to_fraction a) = f1)
-      [elim z
-        [simplify.
-         rewrite > H2.rewrite > H1.simplify.
-         rewrite > Hcut.reflexivity
-        |simplify.
-         rewrite > H2.rewrite > H1.simplify.
-         rewrite > Hcut.reflexivity
-        |simplify.
-         rewrite > H2.rewrite > H1.simplify.
-         rewrite > Hcut.reflexivity
-        ]
-      |generalize in match H.
-       rewrite > H2.rewrite > H1.simplify.
-       intro.destruct H3.assumption
-      ]
-    |elim H1.clear H1.
-     elim z
-      [simplify.
-       rewrite > H2.rewrite > H2.simplify.
-       elim (or_numerator_nfa_one_nfa_proper (finv f1))
-        [elim H1.clear H1.
-         rewrite > H3.simplify.
-         cut (nat_fact_to_fraction a = f1)
-          [rewrite > Hcut.reflexivity
-          |generalize in match H.
-           rewrite > H2.
-           rewrite > H3.
-           rewrite > Qtimes_q_Qone.
-           intro.
-           destruct H1.
-           assumption
-          ]
-        |elim H1.clear H1.
-         generalize in match H.
-         rewrite > H2.
-         rewrite > H3.simplify. 
-         intro.
-         destruct H1.
-         rewrite > Hcut.
-         simplify.reflexivity
-        ]
-      |simplify.rewrite > H2.simplify.
-        elim (or_numerator_nfa_one_nfa_proper (finv f1))
-        [elim H1.clear H1.
-         rewrite > H3.simplify.
-         cut (nat_fact_to_fraction a = f1)
-          [rewrite > Hcut.reflexivity
-          |generalize in match H.
-           rewrite > H2.
-           rewrite > H3.
-           rewrite > Qtimes_q_Qone.
-           intro.
-           destruct H1.
-           assumption
-          ]
-        |elim H1.clear H1.
-         generalize in match H.
-         rewrite > H2.
-         rewrite > H3.simplify. 
-         intro.
-         destruct H1.
-         rewrite > Hcut.
-         simplify.reflexivity
-        ]
-      |simplify.rewrite > H2.simplify.
-        elim (or_numerator_nfa_one_nfa_proper (finv f1))
-        [elim H1.clear H1.
-         rewrite > H3.simplify.
-         cut (nat_fact_to_fraction a = f1)
-          [rewrite > Hcut.reflexivity
-          |generalize in match H.
-           rewrite > H2.
-           rewrite > H3.
-           rewrite > Qtimes_q_Qone.
-           intro.
-           destruct H1.
-           assumption
-          ]
-        |elim H1.clear H1.
-         generalize in match H.
-         rewrite > H2.
-         rewrite > H3.simplify. 
-         intro.
-         destruct H1.
-         rewrite > Hcut.
-         simplify.reflexivity
-        ]
-      ]
-    ]
-  ]
-qed.
-*)
 (*     
 definition numQ:Q \to Z \def
 \lambda q. 
@@ -187,7 +83,7 @@ elim r
   |elim f
     [reflexivity
     |reflexivity
-    |apply Qtimes1.
+    |apply Qtimes_numerator_denominator.
     ]
   ]
 qed.*)
@@ -205,7 +101,7 @@ elim r
   |elim f
     [reflexivity
     |reflexivity
-    |apply Qtimes1.
+    |apply Qtimes_numerator_denominator.
     ]
   ]
 qed.*)