proposition: Theorem points_in_convex : ∀ (f : puis_ser_pol α) pts L, pts = points_of_ps_polynom f → newton_segments f = Some L → ∀ h αh, (h, αh) ∈ pts → β L <= αh + h * (γ L).
proof: Proof. intros f pts L Hpts HL h αh Hαh. remember [ini_pt L; fin_pt L … oth_pts L] as spts. pose proof (list_Q_pair_in_dec h αh spts) as H. subst spts; destruct H as [H| H]. eapply points_in_any_newton_segment in H; [ idtac | eassumption ]. rewrite H; apply Qle_refl. apply Qlt_le_weak. eapply points_not_in_any_newton_segment; try eassumption. split; assumption. Qed.
imports: Utf8 QArith Misc Field2 InSegment ConvexHull Newton NotInSegment Puiseux_base