proposition: Lemma Liouville_lemma2 : forall x : IR, AbsIR (x[-]a) [<=] Two -> AbsIR (P ! x [-] P ! a) [<=] C [*] AbsIR (x [-] a).
proof: Proof. intros x Hle. apply (poly_law_of_mean Ia Ia_fin Ia_proper P a x a_in_Ia (Liouville_lemma1 x Hle)). Qed.
imports: CRing_Homomorphisms CPoly_NthCoeff MoreFunctions Rolle Zlcm Q_can RX_deg QX_ZX QX_root_loc QX_extract_roots