proposition: Theorem make_char_pol_of_pts_eq : ∀ f pts j, make_char_pol R j (List.map (term_of_point f) pts) = make_char_pol_of_pts f j pts.
proof: Proof. intros f pts j. revert j. 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