Even more Q stuff classified.

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

diff --git a/helm/software/matita/library/Q/fraction/ftimes.ma b/helm/software/matita/library/Q/fraction/ftimes.ma
index 2e5871d7390a897df7acfbd48f402d2ec433a2de..bcc7358b27a5ed0b3098c5cbb859a7a12d95a1fd 100644 (file)
--- 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,44 @@ 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;autobatch
+        |cases n7;simplify
+          [autobatch
+          |elim (H2 n9).
+           rewrite > H3.
+           simplify.
+           autobatch
+          ]]]]]
+qed.
\ No newline at end of file