fact: Fixpoint den_list (P : QX) : list Z_as_CRing := match P with | cpoly_zero _ => [1]::nil | cpoly_linear _ c P => Q_can_den c::den_list P end.
imports: CPoly_Degree CoRN.model.rings.Qring Zring Qordfield CRing_Homomorphisms RingClass CRingClass Zlcm Q_can RX_deg