proposition: Lemma Liouville_lemma10 : forall (p : Z_as_CRing) (q : positive), P ! (p#q)%Q [#] [0] -> [1] [<=] (inj_Q_rh q)[^](QX_deg P) [*] C' [*] AbsIR ((inj_Q_rh (p#q)%Q) [-] a).
proof: Proof. intros p q Hap. destruct (Liouville_lemma3 (AbsIR (inj_Q_rh (p # q)%Q[-]a))). apply (leEq_transitive _ _ _ _ (less_leEq _ _ _ c)). apply (leEq_wdl _ ([1] [*] AbsIR (inj_Q_rh (p#q)%Q [-] a))); [|rational]. apply mult_resp_leEq_rht; [|apply AbsIR_nonneg]. apply (leEq_wdl _ ([1] [*] [1])); [|rational]. apply mult_resp_leEq_both; [apply less_leEq; apply pos_one|apply less_leEq; apply pos_one| |apply lft_leEq_Max]. apply Liouville_lemma8. apply (leEq_transitive _ _ _ _ (Liouville_lemma9 _ _ Hap (less_leEq _ _ _ c))). apply mult_resp_leEq_rht; [|apply AbsIR_nonneg]. apply mult_resp_leEq_lft; [|]. unfold C'; apply rht_leEq_Max. 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