proposition: Theorem gamma_value_jh : ∀ f L j αj, newton_segments f = Some L → (j, αj) = ini_pt L → ∀ h αh, (h, αh) ∈ oth_pts L → γ L == (αj - αh) / (h - j).
proof: Proof. intros f L j αj HL Hjαj h αh Hhαh. remember HL as Hh; clear HeqHh. apply points_in_any_newton_segment with (h := h) (αh := αh) in Hh. apply Qeq_plus_minus_eq_r in Hh. remember HL as Haj; clear HeqHaj. apply points_in_any_newton_segment with (h := j) (αh := αj) in Haj. rewrite <- Hh, Haj. field. apply Qlt_not_0. eapply jq_lt_hq; try eassumption. left; rewrite Hjαj; reflexivity. right; right; assumption. Qed.
imports: Utf8 QArith Sorted NPeano ConvexHull ConvexHullMisc Misc NbarM QbarM Newton PolyConvexHull Field2 Fpolynomial PSpolynomial Puiseux_base Power_series Puiseux_series Ps_div Slope_base