proposition: Theorem nth_in_newton_segments_any_r : ∀ f₁ L₁ c₁ fn Ln n, newton_segments f₁ = Some L₁ → c₁ = ac_root (Φq f₁ L₁) → (∀ i, i ≤ n → (ps_poly_nth 0 (nth_pol i f₁ L₁) ≠ 0)%ps) → fn = nth_pol n f₁ L₁ → Ln = nth_ns n f₁ L₁ → newton_segments fn = Some Ln.
proof: Proof. intros f₁ L₁ c₁ fn Ln n HL₁ Hc₁ Hpsi Hfn HLn. subst fn Ln. pose proof (exists_pol_ord K f₁) as H. destruct H as (m, (Hm, Hp)); clear Hm. revert f₁ L₁ c₁ m HL₁ Hp Hc₁ Hpsi. induction n; intros; [ assumption | simpl ]. rewrite <- Hc₁. remember (next_pol f₁ (β L₁) (γ L₁) c₁) as f₂ eqn:Hf₂ . remember (option_get phony_ns (newton_segments f₂)) as L₂ eqn:HL₂ . assert (1 ≤ S n) as H₁ by apply le_n_S, Nat.le_0_l. apply Hpsi in H₁; simpl in H₁. rewrite <- Hc₁, <- Hf₂ in H₁. remember (q_of_m m (γ L₁)) as q₀ eqn:Hq₀ . assert (0 ≤ S n)%nat as H by apply Nat.le_0_l. eapply IHn with (m := (m * q₀)%positive); try eassumption; try reflexivity. eapply next_ns_in_f; eassumption . eapply next_pol_in_K_1_mq; eassumption . intros i Hin. apply Nat.succ_le_mono in Hin. apply Hpsi 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