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
| (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