proposition: Theorem next_ns_r_non_decr : ∀ f L c f₁ L₁ c₁ r 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₁ → r ≤ r₁ → r = 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 r₁. intros HL Hc Hf₁ HL₁ Hc₁ Hnz₁ Hr Hr₁ Hrle. remember HL as H; clear HeqH. eapply next_has_ns in H; try eassumption . rename H into HL₁nz. remember (newton_segments f₁) as Lo eqn:HLo. symmetry in HLo. destruct Lo as [L'₁| ]; [ | easy ]. simpl in HL₁; subst L'₁. generalize HLo; intro H. apply exists_ini_pt_nat in H. destruct H as (j₁, (αj₁, Hini₂)). remember HLo as H; clear HeqH. apply exists_fin_pt_nat in H. destruct H as (k₁, (αk₁, Hfin₂)). remember HL as H; clear HeqH. eapply j_0_k_betw_r₀_r₁ with (c := c) in H; try eassumption . destruct H as (Hj₁, (Hrk₁, (Hk₁r, (Hαj₁, (Hαk₁, Hαk₁z))))). remember Hrle as H; clear HeqH. eapply Nat.le_trans in H; try eassumption . eapply Nat.le_antisymm in H; try eassumption . move H at top; subst r₁. apply Nat.le_antisymm in Hrle; try eassumption . move Hrle at top; subst k₁. split; [ apply eq_refl | ]. destruct Hαk₁z; [ exfalso; revert H; apply Nat.lt_irrefl | idtac ]. subst j₁. exists αj₁, αk₁. split; [ assumption | idtac ]. split; [ assumption | idtac ]. unfold Qlt in Hαj₁; simpl in Hαj₁. unfold Qeq in H; simpl in H. rewrite Z.mul_1_r in Hαj₁, H. split; assumption. now rewrite HLo. 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