proposition: Theorem order_pol_apply_nonneg : ∀ f y, (∀ a, a ∈ al f → (0 ≤ order a)%Qbar) → (0 ≤ order y)%Qbar → (0 ≤ order (ps_pol_apply f y))%Qbar.
proof: Proof. intros f y Ha Hy. unfold ps_pol_apply, apply_poly. remember (al f) as la; clear Heqla. induction la as [| a]; intros; simpl. rewrite order_0; constructor. eapply Qbar.le_trans; [ idtac | apply order_add ]. rewrite order_mul; auto. apply Qbar.min_glb. eapply Qbar.le_trans; eauto . rewrite Qbar.add_comm. apply Qbar.le_sub_le_add_l. rewrite Qbar.sub_diag. apply IHla. intros b Hb. apply Ha; right; assumption. apply Ha; left; reflexivity. Qed.
imports: Utf8 QArith NPeano Sorting Misc Field2 Fpolynomial Fsummation Newton ConvexHull Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq F1Prop Q_field PosOrder QbarM