proposition: Theorem fold_char_pol : ∀ f j αj tl, [order_coeff (List.nth j (al f) 0%ps) … make_char_pol R (S j) (List.map (term_of_point f) tl)] = make_char_pol R j (List.map (term_of_point f) [(Qnat j, αj) … tl]).
proof: Proof. intros f j αj tl; simpl. rewrite nat_num_Qnat, Nat.sub_diag; simpl. reflexivity. Qed.
imports: Utf8 QArith Sorted NPeano ConvexHull ConvexHullMisc Misc NbarM QbarM Newton PolyConvexHull Field2 Fpolynomial PSpolynomial Puiseux_base Power_series Puiseux_series Ps_div Slope_base