proposition: Lemma QX_root_loc : forall (P : QX) (a : Q_as_CRing), P ! [0] [#] [0] -> P ! a [=] [0] -> In (Q_can a) (list_Q (P0 P) (Pn P)).
proof: Proof. intros P a Hap Hval. apply list_Q_spec. intro; apply Hap; clear Hap. unfold P0 in H. cut ((_C_ (Zlcm_den_poly P:Q_as_CRing) [*] P) ! [0] [=] [0]). rewrite -> mult_apply, c_apply. intro H0; apply (Qmult_integral_l (Zlcm_den_poly P)); [|assumption]. intro H1; destruct (Zlcm_den_poly_nz P). unfold Qeq in H1; simpl in H1. rewrite Zmult_1_r in H1; assumption. cut ((zx2qx (qx2zx P)) ! [0] [=] [0]). rewrite -> qx2zx_spec; tauto. unfold zx2qx. rewrite <- (rh_pres_zero _ _ injZ_rh) at 1. rewrite <- cpoly_map_apply. cut ((qx2zx P) ! [0] [=] [0]). intro H0; rewrite H0; reflexivity. rewrite -> poly_at_zero; assumption. case (QX_dec P [0]). intro H; destruct Hap; rewrite -> H; reflexivity. intros Hap2 Heq; apply (ap_imp_neq _ _ _ Hap2); clear Hap Hval; revert Heq. unfold Pn. destruct (RX_deg_spec _ Z_dec (qx2zx P)); [|]. case (ZX_dec (qx2zx P) [0]); [|tauto]. intro Heq; destruct (ap_imp_neq _ _ _ Hap2); clear Hap2. cut (_C_(Zlcm_den_poly P:Q_as_CRing) [*] P [=] [0]). intro Heq2; apply all_nth_coeff_eq_imp; intro i. apply (Qmult_integral_l (Zlcm_den_poly P)). intro H1; destruct (Zlcm_den_poly_nz P). unfold Qeq in H1; simpl in H1. rewrite Zmult_1_r in H1; assumption. generalize (nth_coeff_wd _ i _ _ Heq2). rewrite -> nth_coeff_c_mult_p. simpl; tauto. rewrite <- qx2zx_spec. rewrite -> Heq. apply (rh_pres_zero _ _ zx2qx). intro H; destruct c; fold (ZX_deg (qx2zx P)). rewrite <- qx2zx_deg; assumption. apply den_div_P0; assumption. rewrite inj_Zabs_nat. rewrite <- Q_can_den_pos_val_spec. apply Zdivides_abs_elim_lft. apply den_div_Pn; assumption. Qed.
imports: CPoly_Degree CRing_Homomorphisms Qring Zring Qordfield RingClass CRingClass Zlcm Q_can nat_Q_lists RX_deg QX_ZX