proposition: Theorem order_bbar_nonneg : ∀ f L c₁ r f₁, newton_segments f = Some L → c₁ = ac_root (Φq f L) → r = root_multiplicity acf c₁ (Φq f L) → f₁ = next_pol f (β L) (γ L) c₁ → ∀ i, (order (ps_poly_nth i f₁) ≥ 0)%Qbar.
proof: Proof. intros f L c₁ r f₁ HL Hc₁ Hr Hf₁ i. remember (quotient_phi_x_sub_c_pow_r (Φq f L) c₁ r) as Ψ eqn:HΨ . remember HL as Hini; clear HeqHini. apply exists_ini_pt_nat in Hini. destruct Hini as (j, (αj, Hini)). rewrite f₁_eq_term_with_Ψ_plus_g; try eassumption. unfold ps_poly_nth; simpl. rewrite fold_ps_lap_add. rewrite ps_lap_nth_add. rewrite fold_ps_lap_comp. eapply Qbar.le_trans; [ idtac | apply order_add ]. apply Qbar.min_glb. rewrite <- lap_mul_assoc. rewrite fold_ps_lap_mul, fold_ps_lap_pow. destruct (le_dec r i) as [Hle| Hgt]. rewrite ps_lap_nth_x_le_pow_mul; [ idtac | assumption ]. progress unfold ps_lap_comp. rewrite monom_y_plus_c_is_inject_K. rewrite fold_ps_lap_pow. rewrite lap_power_map_ps. rewrite fold_ps_lap_comp. rewrite lap_inject_comp. rewrite fold_ps_lap_mul. rewrite lap_inject_mul. apply order_nth_inject_K. apply Nat.nle_gt in Hgt. rewrite ps_lap_nth_x_gt_pow_mul; [ idtac | assumption ]. rewrite order_0; constructor. apply Qbar.lt_le_incl. apply nth_g_order_pos; assumption. Qed.
imports: Utf8 QArith NPeano Sorted Misc QbarM SplitList Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull Puiseux_base Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial AlgCloCharPol CharactPolyn F1Eq PosOrder InK1m