proposition: Theorem gamma_value_jk : ∀ L j k αj αk, (j, αj) = ini_pt L → (k, αk) = fin_pt L → γ L = (αj - αk) / (k - j).
proof: Proof. intros L j k αj αk Hjαj Hkαk. unfold γ; simpl. rewrite <- Hjαj, <- Hkαk; reflexivity. 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