proposition: Theorem r₁_le_r₀ : ∀ f L f₁, newton_segments f = Some L → f₁ = nth_pol 1 f L → (ps_poly_nth 0 f₁ ≠ 0)%ps → nth_r 1 f L ≤ nth_r 0 f L.
proof: Proof. intros f L f₁ HL Hf₁ Hnz₀; simpl. simpl in Hf₁; rewrite <- Hf₁. remember (ac_root (Φq f L)) as c eqn:Hc . remember (option_get phony_ns (newton_segments f₁)) as L₁ eqn:HL₁ . remember (ac_root (Φq f₁ L₁)) as c₁ eqn:Hc₁ . 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; eauto with Arith. destruct H as (Hj₁, (Hr₁, (Hr, _))). transitivity k₁; 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