proposition: Theorem fold_qpower_list : ∀ pow (psl : list (puiseux_series α)), List.map (pair_rec (λ pow ps, (Qnat pow, ps))) (power_list pow psl) = qpower_list pow psl.
proof: Proof. reflexivity. Qed.
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