fact: Definition coeff_of_pt f i (pts : list (Q * Q)) := coeff_of_hl (al f) i (List.map (λ pt, nat_num (fst pt)) pts).
imports: Utf8 QArith NPeano Sorted ConvexHullMisc ConvexHull PolyConvexHull Field2 Misc Newton NbarM QbarM SplitList Fsummation Fpolynomial Power_series Puiseux_series Ps_add Ps_mul Ps_div Ps_add_compat PSpolynomial Puiseux_base CharactPolyn AlgCloCharPol