proposition: Theorem order_root_tail_nonneg_any_r : ∀ f L c f₁ L₁ m q₀ n r, newton_segments f = Some L → m = ps_pol_com_polydo f → q₀ = q_of_m m (γ L) → c = ac_root (Φq f L) → f₁ = next_pol f (β L) (γ L) c → L₁ = option_get phony_ns (newton_segments f₁) → zerop_1st_n_const_coeff n f L = false → root_multiplicity acf c (Φq f L) = r → (∀ i, r ≤ nth_r i f L) → (0 ≤ order (root_tail (m * q₀) n f₁ L₁))%Qbar.
proof: Proof. intros f L c f₁ L₁ m q₀ n r. intros HL HK Hq₀ Hc Hf₁ HL₁ Hz Hr Hrle. rewrite zerop_1st_n_const_coeff_false_iff in Hz. pose proof (Hz O (Nat.le_0_l n)) as H; simpl in H. rename H into Hnz; move Hnz before Hc. apply zerop_1st_n_const_coeff_false_iff in Hz. remember (zerop_1st_n_const_coeff n f₁ L₁) as z₁ eqn:Hz₁ . symmetry in Hz₁. destruct z₁. unfold root_tail. rewrite Hz₁. rewrite order_0; constructor. eapply order_root_tail_nonneg_any_r_aux with (r := r); try eassumption. pose proof (exists_pol_ord K f) as H. destruct H as (m', (Hm', Hp)). rewrite <- HK in Hm'; subst m'. apply Hp. apply not_zero_1st_prop; [ simpl | assumption ]. rewrite <- Hc, <- Hf₁, <- HL₁; assumption. apply non_decr_imp_eq; try assumption. rewrite zerop_1st_n_const_coeff_succ; simpl. rewrite <- Hc, <- Hf₁, <- HL₁; rewrite Hz₁. remember (ps_poly_nth 0 f) as x. destruct (ps_zerop K x); [ contradiction | reflexivity ]. simpl; rewrite <- Hc; assumption. Qed.
imports: Utf8 QArith NPeano Sorting Misc SlopeMisc Slope_base QbarM NbarM Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull PolyConvexHull NotInSegment Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq PosOrder F1Prop InK1m Q_field RootHeadTail RootAnyR