proposition: Lemma Liouville_lemma9 : forall (p : Z_as_CRing) (q : positive), P ! (p#q)%Q [#] [0] -> AbsIR ((inj_Q_rh (p#q)%Q) [-] a) [<=] Two -> [1] [<=] (inj_Q_rh q)[^](QX_deg P) [*] C [*] AbsIR ((inj_Q_rh (p#q)%Q) [-] a).
proof: Proof. intros p q Hap Hle. apply (leEq_transitive _ _ _ _ (Liouville_lemma7 _ _ Hap)). rewrite <- CRings.mult_assoc, <- CRings.mult_assoc. apply mult_resp_leEq_lft. unfold C. rewrite <- CRings.mult_assoc. apply mult_resp_leEq_lft; [|apply AbsIR_nonneg]. apply (leEq_wdl _ _ _ _ (Liouville_lemma2 _ _ _ Hle)). apply AbsIR_wd. rewrite -> Ha. rewrite -> cg_inv_zero. unfold inj_QX_rh. rewrite -> cpoly_map_apply; reflexivity. set (Liouville_lemma8 (QX_deg P) q). apply (leEq_transitive _ _ [1]); [apply less_leEq; apply pos_one|]. apply Liouville_lemma8. Qed.
imports: CRing_Homomorphisms CPoly_NthCoeff MoreFunctions Rolle Zlcm Q_can RX_deg QX_ZX QX_root_loc QX_extract_roots