fact: Fixpoint filter_finite_ord α (r : ring α) {K : field r} (dpl : list (Q * puiseux_series α)) := match dpl with | [(pow, ps) … dpl₁] => match order ps with | qfin v => [(pow, v) … filter_finite_ord dpl₁] | qinf => filter_finite_ord dpl₁ end | [] => [] end.
imports: Utf8 QArith Sorting ConvexHull ConvexHullMisc Misc NbarM QbarM Newton Field2 Fpolynomial Power_series Puiseux_series Ps_add Ps_add_compat Ps_mul Ps_div