proposition: Lemma QX_extract_roots_spec_rat : forall P a, P [#] [0] -> (QX_extract_roots P) ! a [#] [0].
proof: Proof. unfold QX_extract_roots. intros P a; remember (QX_deg P) as n; revert P Heqn. induction n. intros P Hdeg Hap; unfold QX_extract_roots_rec. destruct (RX_deg_spec _ Q_dec _ Hap). fold QX_deg in d; rewrite <- Hdeg in d. destruct (degree_le_zero _ _ d). case (Q_dec P ! a [0]); [|tauto]. intro Heq; destruct (ap_imp_neq _ _ _ Hap); clear Hap; revert Heq. rewrite -> s, c_apply; intro H; rewrite -> H; split; [reflexivity|apply I]. unfold QX_extract_roots_rec. intros P Hdeg Hap. case_eq (QX_find_root P). intros x Hsome; fold (QX_extract_roots_rec n (RX_div _ P x)). apply IHn. apply eq_add_S. rewrite <- QX_div_deg; [assumption|]. rewrite <- Hdeg; discriminate. case (QX_dec (RX_div _ P x) [0]); [|tauto]. intro Heq; apply QX_div_deg0. rewrite <- Hdeg; discriminate. intro; apply QX_find_root_spec_none; 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