proposition: Theorem r_n_nth_ns : ∀ f L c f₁ L₁ c₁ m r, newton_segments f = Some L → pol_in_K_1_m f m → c = ac_root (Φq f L) → f₁ = next_pol f (β L) (γ L) c → L₁ = option_get phony_ns (newton_segments f₁) → c₁ = ac_root (Φq f₁ L₁) → ∀ n fn Ln, (∀ i, (i ≤ n)%nat → (ps_poly_nth 0 (nth_pol i f₁ L₁) ≠ 0)%ps) → (∀ i, (i ≤ S n)%nat → (nth_r i f L = r)) → fn = nth_pol n f₁ L₁ → Ln = nth_ns n f₁ L₁ → ∃ αj αk, ini_pt Ln = (Qnat 0, αj) ∧ fin_pt Ln = (Qnat r, αk) ∧ (0 < Qnum αj)%Z ∧ Qnum αk = 0%Z.
proof: Proof. intros f L c f₁ L₁ c₁ m r HL Hm Hc Hf₁ HL₁ Hc₁. intros n fn Ln Hpsi Hri Hfn HLn. destruct r. pose proof (Hri O (Nat.le_0_l (S n))) as H. simpl in H. rewrite <- Hc in H. eapply multiplicity_neq_0 in HL; [ | eassumption ]. contradiction. remember (S r) as r'. assert (0 < r')%nat as Hrnz by (subst r'; apply Nat.lt_0_succ). clear r Heqr'; rename r' into r. remember (q_of_m m (γ L)) as q₀ eqn:Hq₀ . revert fn Ln Hpsi Hfn HLn. revert f L c f₁ L₁ c₁ m q₀ r HL Hm Hq₀ Hc Hc₁ Hf₁ HL₁ Hri Hrnz. induction n; intros. pose proof (Hpsi O (Nat.le_0_l O)) as Hnz; simpl in Hnz. simpl in Hfn, HLn; subst fn Ln. remember HL as H; clear HeqH. eapply r_n_next_ns in H; try eassumption. pose proof (Hri O Nat.le_0_1) as Hr; simpl in Hr. rewrite <- Hc in Hr; assumption. pose proof (Hri 1%nat (Nat.le_refl 1)) as Hr₁; simpl in Hr₁. rewrite <- Hc, <- Hf₁, <- HL₁, <- Hc₁ in Hr₁; assumption. pose proof (Hpsi O (Nat.le_0_l (S n))) as H; simpl in H. rename H into Hnz₁. remember HL as H; clear HeqH. eapply r_n_next_ns with (L₁ := L₁) (r := r) in H; try eassumption. destruct H as (αj₁, (αk₁, H)). destruct H as (Hini₁, (Hfin₁, (Hαj₁, Hαk₁))). remember HL₁ as H; clear HeqH. eapply hd_newton_segments in H; try eassumption. rename H into HL₁i. simpl in Hfn, HLn. rewrite <- Hc₁ in Hfn, HLn. remember (next_pol f₁ (β L₁) (γ L₁) c₁) as f₂ eqn:Hf₂ . remember (option_get phony_ns (newton_segments f₂)) as L₂ eqn:HL₂ . eapply IHn with (L := L₁) (L₁ := L₂) (m := (m * q₀)%positive); try eassumption; try reflexivity. eapply next_pol_in_K_1_mq with (L := L); eassumption . intros i Hin. apply le_n_S in Hin. apply Hri in Hin; simpl in Hin. rewrite <- Hc, <- Hf₁, <- HL₁ in Hin. assumption. intros i Hin. apply le_n_S in Hin. apply Hpsi in Hin; simpl in Hin. rewrite <- Hc₁, <- Hf₂, <- HL₂ in Hin. assumption. assert (0 ≤ S (S n)) as H₁ by apply Nat.le_0_l. apply Hri in H₁; simpl in H₁. rewrite <- Hc in H₁; assumption. assert (0 ≤ S n) as H₁ by apply Nat.le_0_l. apply Nat.succ_le_mono in H₁. apply Hri in H₁; simpl in H₁. rewrite <- Hc, <- Hf₁, <- HL₁, <- Hc₁ in H₁; 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