fact: Fixpoint coeff_of_hl la i hl := match hl with | [] => 0%K | [h … hl₁] => if eq_nat_dec i h then order_coeff (List.nth h la 0%ps) else coeff_of_hl la i hl₁ end.
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