proposition: Lemma poly_law_of_mean : forall a b, I a -> I b -> AbsIR (P ! b [-] P ! a) [<=] C [*] (AbsIR (b [-] a)).
proof: Proof. intros a b Ha Hb. set (Law_of_the_Mean_Abs_ineq I I_proper (FPoly IR P) (FPoly IR (_D_ P)) Hderiv a b Ha Hb (CPoly_bound I I_fin (_D_ P))). simpl in c. apply c; [|auto|auto]. clear c; intros x Hcomp Htrue; clear Htrue. apply CPoly_bound_spec. destruct Hcomp. destruct I; simpl in *; try auto; try split; try (destruct Ha; destruct Hb); (apply (less_leEq_trans _ _ (MIN a b)); [apply less_Min|]; assumption)|| (apply (leEq_less_trans _ _ (MAX a b)); [|apply Max_less]; assumption)|| (apply (leEq_transitive _ _ (MIN a b)); [apply leEq_Min|]; assumption)|| (apply (leEq_transitive _ _ (MAX a b)); [|apply Max_leEq]; assumption). Qed.
imports: CRing_Homomorphisms CPoly_NthCoeff MoreFunctions Rolle Zlcm Q_can RX_deg QX_ZX QX_root_loc QX_extract_roots