proposition: Lemma QX_find_root_spec_none : forall P, QX_find_root P = None -> forall q : Q_as_CRing, P ! q [#] [0].
proof: Proof. intro P; unfold QX_find_root. case (Q_dec P ! [0] [0]). intros; discriminate. intros Hap Hnone q. assert (forall x y : Q_as_CRing, {x = y} + {x <> y}). clear; intros x y. destruct x; destruct y; simpl. case (Z.eq_dec Qnum Qnum0); case (Z.eq_dec Qden Qden0); intros H1 H2. left; f_equal; [assumption|injection H1; tauto]. right; intro H3; injection H3; intros; destruct H1; f_equal; assumption. right; intro H3; injection H3; intros; destruct H2; assumption. right; intro H3; injection H3; intros; destruct H2; assumption. destruct (In_dec X (Q_can q) (list_Q (P0 P) (Pn P))). intro H; rewrite -> (Q_can_spec q) in H; revert H. apply (QX_test_list_spec_none _ _ Hnone _ i). intro Hval; apply n. apply QX_root_loc; 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