proposition: Lemma QX_find_root_spec_some : forall P x, QX_find_root P = Some x -> P ! x [=] [0].
proof: Proof. intros P x; unfold QX_find_root. case (Q_dec P ! [0] [0]). intros H1 H2; injection H2; intro H3; rewrite <- H3; assumption. intro Hap; apply QX_test_list_spec_some. Qed.
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