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