fact: Definition nat_prod_to_Q (pq : nat * nat) : list Q_as_CRing := let (p, q) := pq in match p with | O => Qmake Z0 (P_of_succ_nat q)::nil | S p => match q with | O => nil | S q => Qmake (Zpos (P_of_succ_nat p)) (P_of_succ_nat q):: Qmake (Zneg (P_of_succ_nat p)) (P_of_succ_nat q)::nil end end.
imports: Zring Qring Q_can