proposition: Theorem al_Φq : ∀ f L, al (Φq f L) = make_char_pol R (nat_num (fst (ini_pt L))) (List.map (term_of_point f) [ini_pt L … oth_pts L ++ [fin_pt L]]).
proof: Proof. intros f L; 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