fact: Fixpoint Q_can_num_poly (P : QX) : ZX := match P with | cpoly_zero _ => cpoly_zero Z_as_CRing | cpoly_linear _ c Q => cpoly_linear Z_as_CRing (Q_can_num c) (Q_can_num_poly Q) end.
imports: CPoly_Degree CoRN.model.rings.Qring Zring Qordfield CRing_Homomorphisms RingClass CRingClass Zlcm Q_can RX_deg