proposition: Theorem first_n_pol_in_K_1_m_any_r : ∀ f L fn m c r, newton_segments f = Some L → pol_in_K_1_m f m → c = ac_root (Φq f L) → q_of_m m (γ L) = 1%positive → root_multiplicity acf c (Φq f L) = r → (∀ i, r ≤ nth_r i f L) → ∀ n, (∀ i, 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 fn m c r HL HK Hc Hq Hr Hri n Hnz Hfn. revert f L fn m c HL HK Hc Hq Hr Hri Hnz Hfn. induction n; intros. simpl in Hfn; subst fn; assumption. remember (next_pol f (β L) (γ L) c) as f₁ eqn:Hf₁ . remember (option_get phony_ns (newton_segments f₁)) as L₁ eqn:HL₁ . remember HL₁ as H; clear HeqH. apply exists_ini_pt_nat_fst_seg in H. destruct H as (j₁, (αj₁, Hini₁)). remember HL₁ as H; clear HeqH. apply exists_fin_pt_nat_fst_seg in H. destruct H as (k₁, (αk₁, Hfin₁)). remember (ac_root (Φq f₁ L₁)) as c₁ eqn:Hc₁ . simpl in Hfn. rewrite <- Hc, <- Hf₁, <- HL₁ in Hfn. assert (1 ≤ S n)%nat as H by apply le_n_S, Nat.le_0_l. apply Hnz in H; simpl in H. rewrite <- Hc, <- Hf₁ in H. rename H into Hnz₁. remember HL as H; clear HeqH. eapply next_ns_in_f in H; try eassumption. rename H into HL₁i. remember HL as H; clear HeqH. eapply q_eq_1_r_non_decr in H; try eassumption. rename H into Hq₁. remember (root_multiplicity acf c₁ (Φq f₁ L₁)) as r₁ eqn:Hr₁ . pose proof (Hri 1%nat) as H; simpl in H. rewrite <- Hc, <- Hf₁, <- HL₁, <- Hc₁ in H. rewrite <- Hr₁ in H. rename H into Hrr. remember HL as H; clear HeqH. symmetry in Hr₁. eapply next_ns_r_non_decr in H; try eassumption. destruct H as (H, _); move H at top; subst r₁. clear Hrr. eapply IHn with (f := f₁); try eassumption. replace m with (m * 1)%positive by apply Pos.mul_1_r. symmetry in Hq. eapply next_pol_in_K_1_mq with (L := L); try eassumption. eapply all_r_le_next with (f := f); try eassumption . intros i Hin. apply Nat.succ_le_mono in Hin. apply Hnz in Hin; simpl in Hin. rewrite <- Hc, <- Hf₁, <- HL₁ in Hin. 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