(* *)
(**************************************************************************)
+include "Q/q/qinv.ma".
+
(*
let rec nat_fact_to_fraction_inv l \def
match l with
qed.
*)
-(* la prova seguente e' tutta una ripetizione. Sistemare. *)
-(*CSC
-theorem Qtimes1: \forall f:fraction.
-Qtimes (nat_fact_all_to_Q (numerator f))
-(Qinv (nat_fact_all_to_Q (numerator (finv 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
- |simplify.
- rewrite > H2.rewrite > H1.simplify.
- rewrite > Hcut.reflexivity
- |simplify.
- rewrite > H2.rewrite > H1.simplify.
- rewrite > Hcut.reflexivity
- ]
- |generalize in match H.
- rewrite > H2.rewrite > H1.simplify.
- intro.destruct H3.assumption
- ]
- |elim H1.clear H1.
- elim z
- [simplify.
- rewrite > H2.rewrite > H2.simplify.
- elim (or_numerator_nfa_one_nfa_proper (finv f1))
- [elim H1.clear H1.
- rewrite > H3.simplify.
- cut (nat_fact_to_fraction a = f1)
- [rewrite > Hcut.reflexivity
- |generalize in match H.
- rewrite > H2.
- rewrite > H3.
- rewrite > Qtimes_q_Qone.
- intro.
- destruct H1.
- assumption
- ]
- |elim H1.clear H1.
- generalize in match H.
- rewrite > H2.
- rewrite > H3.simplify.
- intro.
- destruct H1.
- rewrite > Hcut.
- simplify.reflexivity
- ]
- |simplify.rewrite > H2.simplify.
- elim (or_numerator_nfa_one_nfa_proper (finv f1))
- [elim H1.clear H1.
- rewrite > H3.simplify.
- cut (nat_fact_to_fraction a = f1)
- [rewrite > Hcut.reflexivity
- |generalize in match H.
- rewrite > H2.
- rewrite > H3.
- rewrite > Qtimes_q_Qone.
- intro.
- destruct H1.
- assumption
- ]
- |elim H1.clear H1.
- generalize in match H.
- rewrite > H2.
- rewrite > H3.simplify.
- intro.
- destruct H1.
- rewrite > Hcut.
- simplify.reflexivity
- ]
- |simplify.rewrite > H2.simplify.
- elim (or_numerator_nfa_one_nfa_proper (finv f1))
- [elim H1.clear H1.
- rewrite > H3.simplify.
- cut (nat_fact_to_fraction a = f1)
- [rewrite > Hcut.reflexivity
- |generalize in match H.
- rewrite > H2.
- rewrite > H3.
- rewrite > Qtimes_q_Qone.
- intro.
- destruct H1.
- assumption
- ]
- |elim H1.clear H1.
- generalize in match H.
- rewrite > H2.
- rewrite > H3.simplify.
- intro.
- destruct H1.
- rewrite > Hcut.
- simplify.reflexivity
- ]
- ]
- ]
- ]
-qed.
-*)
(*
definition numQ:Q \to Z \def
\lambda q.
|elim f
[reflexivity
|reflexivity
- |apply Qtimes1.
+ |apply Qtimes_numerator_denominator.
]
]
qed.*)
|elim f
[reflexivity
|reflexivity
- |apply Qtimes1.
+ |apply Qtimes_numerator_denominator.
]
]
qed.*)