proposition: Theorem nth_pol_in_K_1_m : ∀ f L c αj αk fn m n r, newton_segments f = Some L → pol_in_K_1_m f m → c = ac_root (Φq f L) → ini_pt L = (Qnat 0, αj) → fin_pt L = (Qnat r, αk) → (0 < Qnum αj)%Z → Qnum αk = 0%Z → root_multiplicity acf c (Φq f L) = r → (∀ n, r ≤ nth_r n f L) → (∀ i : nat, i ≤ n → (ps_poly_nth 0 (nth_pol i f L) ≠ 0)%ps) → fn = nth_pol n f L → pol_in_K_1_m fn m.
proof: Proof. intros f L c αj αk fn m n r. intros HL HK Hc Hini Hfin Hαj Hαk Hr Hrle Hpsi Hfn. eapply first_n_pol_in_K_1_m_any_r; try eassumption. symmetry in Hr. eapply q_eq_1_any_r; try eassumption. reflexivity. 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