-set "baseuri" "cic:/matita/Q/frac".
-
-include "nat/factorization.ma".
-include "Q/q.ma".
-
-
-definition numeratorQ \def
-\lambda q.match q with
- [OQ \Rightarrow nfa_zero
- |Qpos r \Rightarrow
- match r with
- [one \Rightarrow nfa_one
- |frac x \Rightarrow numerator x
- ]
- |Qneg r \Rightarrow
- match r with
- [one \Rightarrow nfa_one
- |frac x \Rightarrow numerator x
- ]
- ]
-.
-
-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))
- ]
-.
-
-theorem numeratorQ_nat_fact_all_to_Q: \forall g.
-numeratorQ (nat_fact_all_to_Q g) = g.
-intro.cases g
- [reflexivity
- |reflexivity
- |apply numerator_nat_fact_to_fraction
- ]
-qed.
-
-definition nat_to_Q \def
-\lambda n. nat_fact_all_to_Q (factorize n).
-