proposition: Theorem not_zerop_imp_nth_r_eq_r : ∀ f L f₁ L₁ r b, newton_segments f = Some L → f₁ = next_pol f (β L) (γ L) (ac_root (Φq f L)) → L₁ = option_get phony_ns (newton_segments f₁) → (ps_poly_nth 0 f₁ ≠ 0)%ps → (∀ i : nat, i ≤ 1 → nth_r i f L = r) → zerop_1st_n_const_coeff b (nth_pol 1 f₁ L₁) (nth_ns 1 f₁ L₁) = false → (∀ n : nat, r ≤ nth_r n f L) → ∀ n : nat, n ≤ S b → nth_r n f₁ L₁ = r.
proof: Proof. intros f L f₁ L₁ r b HL Hf₁ HL₁ Hnz₁ Hri Hpsi Hrle. apply non_decr_imp_eq; try eassumption. eapply next_ns_in_f; try eassumption; reflexivity. apply zerop_1st_n_const_coeff_false_succ; assumption. pose proof (Hri 1%nat (Nat.le_refl 1)) as H; simpl in H. rewrite <- Hf₁, <- HL₁ in H; assumption. intros i. pose proof (Hrle (S i)) as H; simpl in H. rewrite <- Hf₁, <- HL₁ 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