proposition: Lemma CPoly_bound_spec : forall x P, I x -> AbsIR (P ! x) [<=] CPoly_bound P.
proof: Proof. intros x P HI. destruct (Cpoly_ex_degree _ P) as [n Hdeg]. destruct (Cpoly_ex_degree _ (AbsPoly P)) as [m HdegA]. unfold CPoly_bound. generalize (degree_le_mon _ _ _ _ (Nat.le_max_l n m) Hdeg). generalize (degree_le_mon _ _ _ _ (Nat.le_max_r n m) HdegA). revert HI. generalize (Nat.max n m). clear. intros n HI HdegP HdegA. rewrite -> (poly_as_sum _ _ _ HdegP). rewrite -> (poly_as_sum _ _ _ HdegA). apply (leEq_transitive _ _ (Sum 0 n (fun i => AbsIR (nth_coeff i P[*]x[^]i)))). apply triangle_SumIR. apply Nat.le_0_l. apply Sum_resp_leEq. apply Nat.le_0_l. intros i H1 H2. rewrite -> AbsIR_resp_mult. rewrite -> Abs_poly_nth_coeff. apply mult_resp_leEq_lft; [|apply AbsIR_nonneg]. rewrite -> AbsIR_nexp_op. apply nexp_resp_leEq; [apply AbsIR_nonneg|]. apply Abs_min_max; assumption. Qed.
imports: CRing_Homomorphisms CPoly_NthCoeff MoreFunctions Rolle Zlcm Q_can RX_deg QX_ZX QX_root_loc QX_extract_roots