proposition: Theorem coeff_of_term_pt_eq : ∀ f pts i, coeff_of_term i (List.map (term_of_point f) pts) = coeff_of_pt f i pts.
proof: Proof. intros f pts i. progress unfold coeff_of_pt; simpl. revert i. induction pts as [| (h, ah)]; intros; [ reflexivity | simpl ]. rewrite IHpts; reflexivity. Qed.
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