proposition: Theorem r_n_next_ns : ∀ f L c f₁ L₁ c₁ r, newton_segments f = Some L → 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₁) → (ps_poly_nth 0 f₁ ≠ 0)%ps → root_multiplicity acf c (Φq f L) = r → root_multiplicity acf c₁ (Φq f₁ L₁) = r → ∃ αj αk, ini_pt L₁ = (Qnat 0, αj) ∧ fin_pt L₁ = (Qnat r, αk) ∧ (0 < Qnum αj)%Z ∧ Qnum αk = 0%Z.
proof: Proof. intros f L c f₁ L₁ c₁ r. intros HL Hc Hf₁ HL₁ Hc₁ Hps₀ Hr Hr₁. 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 HL₁ as H; clear HeqH. eapply j_0_k_betw_r₀_r₁ in H; try eassumption. destruct H as (Hj, (Hrk, (Hkr, (Haj, (Hak, Hrak))))). apply Nat.le_antisymm in Hrk; [ | assumption ]. subst j₁ k₁. exists αj₁, αk₁. split; [ assumption | ]. split; [ assumption | ]. destruct Hrak as [H| H]; [ exfalso; revert H; apply Nat.lt_irrefl | idtac ]. unfold Qlt in Haj. unfold Qeq in H. simpl in Haj, H. rewrite Z.mul_1_r in Haj, H. split; 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