fact: Fixpoint QX_test_list (P : QX) (l : list Q_as_CRing) : option Q_as_CRing := match l with | nil => None | cons q l => match Q_dec (P ! q) [0] with inl _ => Some q | inr _ => QX_test_list P l end end.
imports: CPoly_Degree CRing_Homomorphisms CoRN.model.ordfields.Qordfield CauchySeq Q_in_CReals CPoly_Euclid RingClass CRingClass Q_can nat_Q_lists RX_deg RX_div QX_root_loc