proposition: Lemma Liouville_lemma6 : forall (p : Z_as_CRing) (q : positive), P ! (p#q)%Q [#] [0] -> [1] [<=] (inj_Q_rh q)[^](QX_deg P) [*] AbsIR (inj_Q_rh ((Zlcm_den_poly P:Q_as_CRing)[*]P ! (p#q)%Q)).
proof: Proof. intros p q Hap. assert ((zx2qx (qx2zx P)) ! (p#q)%Q[#][0]). case (Q_dec ((zx2qx (qx2zx P)) ! (p#q)%Q) [0]); [|tauto]. intro Heq; destruct (ap_imp_neq _ _ _ Hap); revert Heq. rewrite -> qx2zx_spec. rewrite -> mult_apply, c_apply. intro Heq. apply (mult_eq_zero _ (Zlcm_den_poly P:Q_as_CField)). replace (cm_unit Q_as_CField) with (inject_Z (cm_unit Z_as_CRing)) by reflexivity. intro Heq2; rewrite Q.Qeq_Zeq in Heq2. apply (eq_imp_not_ap _ (Zlcm_den_poly P) [0]). assumption. apply Zlcm_den_poly_nz. assumption. rewrite -> qx2zx_deg; fold ZX_deg. apply (leEq_wdr _ _ _ _ (Liouville_lemma5 _ _ _ X)); fold ZX_deg. apply mult_wdr. apply AbsIR_wd. apply csf_wd. rewrite -> qx2zx_spec. rewrite -> mult_apply, c_apply; reflexivity. Qed.
imports: CRing_Homomorphisms CPoly_NthCoeff MoreFunctions Rolle Zlcm Q_can RX_deg QX_ZX QX_root_loc QX_extract_roots