proposition: Theorem f₁_orders : ∀ 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) ∧ (∀ i, (i < r)%nat → (order (ps_poly_nth i f₁) > 0)%Qbar) ∧ (order (ps_poly_nth r f₁) = 0)%Qbar.
proof: Proof. intros f L c₁ r f₁ HL Hc₁ Hr Hf₁. split; [ eapply order_bbar_nonneg; eassumption | idtac ]. split; [ eapply order_bbar_pos; eassumption | idtac ]. pose proof (exists_pol_ord f) as H. destruct H as (m, (Hm, Hp)). eapply order_bbar_r_is_0; eassumption. 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