+interpretation "Rationals" 'Q = Q.
+
+definition Qone ≝ Qpos one.
+
+definition Qopp ≝
+ λq.
+ match q with
+ [ OQ ⇒ OQ
+ | Qpos r ⇒ Qneg r
+ | Qneg r ⇒ Qpos r
+ ].
+
+definition nat_fact_all_to_Q \def
+\lambda n.
+ match n with
+ [nfa_zero \Rightarrow OQ
+ |nfa_one \Rightarrow Qpos one
+ |nfa_proper l \Rightarrow Qpos (frac (nat_fact_to_fraction l))
+ ].
+
+definition nat_to_Q ≝ λn.nat_fact_all_to_Q (factorize n).
+
+definition Z_to_Q ≝
+ λz.
+ match z with
+ [ OZ ⇒ OQ
+ | pos n ⇒ nat_to_Q (S n)
+ | neg n ⇒ Qopp (nat_to_Q (S n))