(* *)
(**************************************************************************)
+include "Q/q/qinv.ma".
+
(*
let rec nat_fact_to_fraction_inv l \def
match l with
qed.
*)
-Qtimes1 == Qtimes_numerator_denominator
-
(*
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.*)