proposition: Theorem order_bbar_pos : ∀ 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, (i < r)%nat → (order (ps_poly_nth i f₁) > 0)%Qbar.
proof: Proof. intros f L c₁ r f₁ HL Hc₁ Hr Hf₁ i Hir. 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.lt_le_trans; [ idtac | apply order_add ]. apply Qbar.min_glb_lt. rewrite <- lap_mul_assoc. rewrite fold_ps_lap_mul. rewrite fold_ps_lap_pow. rewrite ps_lap_nth_x_gt_pow_mul; [ idtac | assumption ]. rewrite order_0; constructor. 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