X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2Fq%2Fqtimes.ma;h=f03b8687cff5c174ed818cf0471bae3dd864ae44;hb=dc74ed7c4af1aa9b90fc5d2f0a86bd7825696e71;hp=52246e5a57794a159c34d7445c3f0cd6c9c114b8;hpb=7a116453d799657958e32693be28d18a5aab84fc;p=helm.git

diff --git a/helm/software/matita/library/Q/q/qtimes.ma b/helm/software/matita/library/Q/q/qtimes.ma
index 52246e5a5..f03b8687c 100644
--- a/helm/software/matita/library/Q/q/qtimes.ma
+++ b/helm/software/matita/library/Q/q/qtimes.ma
@@ -33,7 +33,7 @@ definition Qtimes : Q \to Q \to Q \def
     ]
   ].
 
-interpretation "rational times" 'times x y = (cic:/matita/Q/q/qtimes/Qtimes.con x y).
+interpretation "rational times" 'times x y = (Qtimes x y).
 
 theorem Qtimes_q_OQ: ∀q. q * OQ = OQ.
  intro;
@@ -189,3 +189,53 @@ cases p
     |apply Qinv_Qtimes;intro;destruct H
     |apply Qinv_Qtimes;intro;destruct H]]
 qed.
+
+theorem Qtimes_numerator_denominator: ∀f:fraction.
+  Qtimes (nat_fact_all_to_Q (numerator f)) (Qinv (nat_fact_all_to_Q (denominator 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
+      |generalize in match H.
+       rewrite > H2.rewrite > H1.simplify.
+       intro.destruct H3.reflexivity
+      ]
+    |elim H1;clear H1;
+     elim z
+      [*:simplify;
+       rewrite > H2;simplify;
+       elim (or_numerator_nfa_one_nfa_proper (finv f1))
+        [1,3,5:elim H1;clear H1;
+         rewrite > H3;simplify;
+         cut (nat_fact_to_fraction a = f1)
+          [1,3,5:rewrite > Hcut;reflexivity
+          |*:generalize in match H;
+           rewrite > H2;
+           rewrite > H3;
+           rewrite > Qtimes_q_Qone;
+           intro;
+           simplify in H1;
+           destruct H1;
+           reflexivity
+          ]
+        |*:elim H1;clear H1;
+         generalize in match H;
+         rewrite > H2;
+         rewrite > H3;simplify;
+         intro;
+         destruct H1;
+         rewrite > Hcut;
+         simplify;reflexivity
+        ]]]]
+qed.
+
+