proposition: Theorem points_not_in_any_newton_segment : ∀ (f : puis_ser_pol α) pts L, pts = points_of_ps_polynom f → newton_segments f = Some L → ∀ h αh, (h, αh) ∈ pts ∧ (h, αh) ∉ [ini_pt L; fin_pt L … oth_pts L] → β L < αh + h * (γ L).
proof: Proof. intros f pts L Hpts HL h αh Hαhnαh. subst pts. eapply points_not_in_any_newton_segment₁; try eassumption. eapply points_of_polyn_sorted; reflexivity. Qed.
imports: Utf8 QArith Misc Field2 InSegment ConvexHull Newton NotInSegment Puiseux_base