proposition: Lemma QX_test_list_spec_none : forall P l, QX_test_list P l = None -> forall q : Q_as_CRing, In q l -> P ! q [#] [0].
proof: Proof. induction l. intros; contradiction. unfold QX_test_list. case (Q_dec P ! a [0]). intros; discriminate. fold (QX_test_list P l). intros Hap Hnone q. simpl (In q (a::l)). case (Q_dec a q). intros Haq Hin Hval. destruct Hap. rewrite -> Haq; assumption. intros. apply IHl. assumption. destruct H. destruct c; rewrite H; reflexivity. 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