Even more Q stuff moved around.

[helm.git] / helm / software / matita / library / Q / q / qtimes.ma

diff --git a/helm/software/matita/library/Q/q/qtimes.ma b/helm/software/matita/library/Q/q/qtimes.ma
index 52246e5a57794a159c34d7445c3f0cd6c9c114b8..3b4b24b7971179f25ca96747d2bef57cc6a7bfad 100644 (file)
--- a/helm/software/matita/library/Q/q/qtimes.ma
+++ b/helm/software/matita/library/Q/q/qtimes.ma
@@ -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.
+
+