proposition: Theorem in_newton_segment_when_r_constant : ∀ f L f₁ L₁ c r, newton_segments f = Some L → c = ac_root (Φq f L) → root_multiplicity acf c (Φq f L) = S r → 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 → (∀ n : nat, S r ≤ nth_r n f L) → ∀ n fn Ln, zerop_1st_n_const_coeff n f₁ L₁ = false → fn = nth_pol n f₁ L₁ → Ln = nth_ns n f₁ L₁ → newton_segments fn = Some Ln.
proof: Proof. intros f L f₁ L₁ c r. intros HL Hc Hr Hf₁ HL₁ Hnz₀ Hrle N polN LN Hz HpolN HLN. rewrite zerop_1st_n_const_coeff_false_iff in Hz. eapply nth_in_newton_segments_any_r with (L₁ := L₁); try eassumption; [ | apply eq_refl ]. generalize HL₁; intros H. pose proof (Hz O (Nat.le_0_l N)) as H₁. rewrite <- Hc in Hf₁. eapply r_n_next_ns in H; try eassumption; try apply eq_refl. destruct H as (αj₁, (αk₁, H)). destruct H as (Hini₁, (Hfin₁, (Hαj₁, Hαk₁))). eapply hd_newton_segments; try eassumption. apply Nat.lt_0_succ. rewrite <- nth_r_n with (n := 1%nat) (f := f) (L := L). symmetry. apply r_le_eq_incl with (n := 1%nat); try assumption. simpl; rewrite <- Hc; assumption. intros i Hi. destruct i; [ assumption | simpl ]. rewrite <- Hc, <- Hf₁, <- HL₁. apply Hz. apply Nat.succ_le_mono in Hi. apply Nat.le_0_r in Hi; subst i. apply Nat.le_0_l. intros; apply Hrle; assumption. apply Nat.le_refl. simpl; rewrite <- Hc; assumption. simpl; rewrite <- Hc, <- Hf₁; assumption. symmetry. apply nth_c_n. simpl; rewrite <- Hc; assumption. simpl; rewrite <- Hc, <- Hf₁; 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 RootAnyR