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