fact: Definition QX_find_root (P : QX) : option Q_as_CRing := match Q_dec (P ! [0]) [0] with inl _ => Some [0] | inr _ => QX_test_list P (list_Q (P0 P) (Pn P)) 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