proposition: Theorem r_le_eq_incl : ∀ f L r n, newton_segments f = Some L → nth_r 0 f L = r → (∀ i, i ≤ n → (ps_poly_nth 0 (nth_pol i f L) ≠ 0)%ps) → (∀ i, i ≤ n → r ≤ nth_r i f L) → (∀ i, i ≤ n → r = nth_r i f L).
proof: Proof. intros f L r n HL Hr₀ Hnz Hri i Hin. remember Hin as H; clear HeqH. apply Hri in H. apply Nat.le_antisymm; auto with Arith. clear H. revert f L r n HL Hr₀ Hnz Hri Hin. induction i; intros; [ rewrite <- Hr₀; reflexivity | idtac ]. destruct n; [ exfalso; revert Hin; apply Nat.nle_succ_0 | idtac ]. remember Hin as H; clear HeqH. apply Hri in H. simpl in H; simpl. remember (ac_root (Φq f L)) as c eqn:Hc . remember (next_pol f (β L) (γ L) c) as f₁ eqn:Hf₁ . remember (option_get phony_ns (newton_segments f₁)) as L₁ eqn:HL₁ . eapply IHi; try eassumption; eauto with Arith. clear H. remember HL as H; clear HeqH. eapply next_has_root_0_or_newton_segments in H; try eassumption; eauto with Arith. destruct H as [H₁| H₁]. assert (1 ≤ S n)%nat as H by apply le_n_S, Nat.le_0_l. apply Hnz in H; contradiction. simpl in H₁. rewrite <- Hc, <- Hf₁ in H₁; auto with Arith. destruct (newton_segments f₁) as [L'₁| ]; [ | easy ]. now subst L₁. apply Nat.le_antisymm. clear H. remember HL as H; clear HeqH. eapply r₁_le_r₀ in H; try eassumption; eauto with Arith. rewrite Hr₀ in H; simpl in H. rewrite <- Hc, <- Hf₁, <- HL₁ in H; auto with Arith. clear H. assert (1 ≤ S n)%nat as H by apply le_n_S, Nat.le_0_l. apply Hnz in H; auto with Arith. clear H. assert (1 ≤ S n)%nat as H by apply le_n_S, Nat.le_0_l. apply Hri in H; simpl in H. rewrite <- Hc, <- Hf₁, <- HL₁ in H; auto with Arith. clear H. intros j Hji. apply Nat.succ_le_mono in Hji. eapply Nat.le_trans in Hin; try eassumption . apply Hnz in Hin; simpl in Hin. rewrite <- Hc, <- Hf₁, <- HL₁ in Hin; auto with Arith. clear H. intros j Hji. apply Nat.succ_le_mono in Hji. eapply Nat.le_trans in Hin; try eassumption . apply Hri in Hin; simpl in Hin. rewrite <- Hc, <- Hf₁, <- HL₁ in Hin; auto with Arith. 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