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