proposition: Lemma Liouville_lemma7 : 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)) [*] AbsIR (inj_Q_rh (P ! (p#q)%Q)).
proof: Proof. intros p q Hap. apply (leEq_wdr _ _ _ _ (Liouville_lemma6 _ _ Hap)). rewrite <- CRings.mult_assoc. apply mult_wdr. rewrite -> rh_pres_mult. apply AbsIR_resp_mult. Qed.
imports: CRing_Homomorphisms CPoly_NthCoeff MoreFunctions Rolle Zlcm Q_can RX_deg QX_ZX QX_root_loc QX_extract_roots