proposition: Lemma QX_test_list_spec_some : forall P l x, QX_test_list P l = Some x -> P ! x [=] [0].
proof: Proof. induction l. intros; discriminate. unfold QX_test_list. fold (QX_test_list P l). case (Q_dec P ! a [0]); [|intro; assumption]. intros. injection H; intro. rewrite <- H0; assumption. 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