X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FQ%2Ffraction%2Fftimes.ma;h=aff8a04a65c23a1c8a015800e9b008525f20a9f1;hb=5431da8145e4a84596d312fc02b552881d119100;hp=2e5871d7390a897df7acfbd48f402d2ec433a2de;hpb=13ee180b4b982b7a150e8d727ed4b83813ac3fa2;p=helm.git

diff --git a/helm/software/matita/library/Q/fraction/ftimes.ma b/helm/software/matita/library/Q/fraction/ftimes.ma
index 2e5871d73..aff8a04a6 100644
--- a/helm/software/matita/library/Q/fraction/ftimes.ma
+++ b/helm/software/matita/library/Q/fraction/ftimes.ma
@@ -14,6 +14,8 @@
 
 include "Q/ratio/ratio.ma".
 include "Q/fraction/finv.ma".
+include "Q/nat_fact/times.ma".
+include "Z/times.ma".
 
 definition nat_frac_item_to_ratio: Z \to ratio \def
 \lambda x:Z. match x with
@@ -88,3 +90,47 @@ intro.elim f.
   | (frac h) \Rightarrow frac (cons (z + - z) h)] = one).
   rewrite > H.rewrite > Zplus_Zopp.reflexivity.
 qed.
+
+theorem times_f_ftimes: \forall n,m.
+frac (nat_fact_to_fraction (times_f n m))
+= ftimes (nat_fact_to_fraction n) (nat_fact_to_fraction m).
+intro.
+elim n
+  [elim m
+    [simplify.
+     rewrite < plus_n_Sm.reflexivity
+    |elim n2
+      [simplify.rewrite < plus_n_O.reflexivity
+      |simplify.reflexivity.
+      ]
+    ]
+  |elim m
+    [elim n1
+      [simplify.reflexivity
+      |simplify.rewrite < plus_n_Sm.reflexivity
+      ]
+    |simplify.
+     cut (\exist h.ftimes (nat_fact_to_fraction n2) (nat_fact_to_fraction n4) = frac h)
+      [elim Hcut.
+       rewrite > H2.
+       simplify.apply eq_f.
+       apply eq_f2
+        [apply eq_plus_Zplus
+        |apply injective_frac.
+         rewrite < H2.
+         apply H
+        ]
+      |generalize in match n4.
+       elim n2
+        [cases n6;simplify;
+          [ exists; [2: autobatch;]
+          | exists; [2:autobatch;]
+          ]
+        |cases n7;simplify
+          [exists;[2:autobatch]
+          |elim (H2 n9).
+           rewrite > H3.
+           simplify.
+           exists;[2:autobatch]
+          ]]]]]
+qed.
\ No newline at end of file