proposition: Lemma QX_extract_roots_spec_nrat : forall (P : QX) (x : IR), (forall y : Q_as_CRing, x [~=] (inj_Q_rh y)) -> (inj_QX_rh P) ! x [=] [0] -> (inj_QX_rh (QX_extract_roots P)) ! x [=] [0].
proof: Proof. intros P x Hx; unfold QX_extract_roots. remember (QX_deg P) as n; revert P Heqn; induction n. intros; unfold QX_extract_roots_rec; assumption. intros P Hdeg Hval; unfold QX_extract_roots_rec; fold (QX_extract_roots_rec). case_eq (QX_find_root P); [|intro; assumption]. intros y Hsome. apply IHn. apply eq_add_S. rewrite Hdeg; apply QX_div_deg. rewrite <- Hdeg; discriminate. clear IHn; revert Hval. rewrite -> (RX_div_spec _ P y) at 1. rewrite -> rh_pres_plus. rewrite -> rh_pres_mult. rewrite -> rh_pres_minus. rewrite -> (cpoly_map_X _ _ inj_Q_rh). rewrite -> (cpoly_map_C _ _ inj_Q_rh). rewrite -> (cpoly_map_C _ _ inj_Q_rh). rewrite -> plus_apply. rewrite -> mult_apply. rewrite -> minus_apply. rewrite -> x_apply. rewrite -> c_apply. rewrite -> c_apply. rewrite -> (QX_find_root_spec_some _ _ Hsome). rewrite -> rh_pres_zero. rewrite -> cm_rht_unit. rewrite -> mult_commutes. set (H := Hx y); revert H; generalize (RX_div Q_as_CRing P y). clear; intros P Hap Heq. apply (mult_eq_zero IR (x[-]inj_Q_rh y)); [|assumption]. intro; apply Hap. apply cg_inv_unique_2; 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