fact: Fixpoint root_head_from_cγ_list α {R : ring α} {K : field R} {acf : algeb_closed_field K} f L b n i := (ps_monom (nth_c (b + i) f L) (γ_sum b i f L) + match n with | O => 0%ps | S n₁ => if ps_zerop K (ps_poly_nth 0 (nth_pol (b + S i) f L)) then 0%ps else root_head_from_cγ_list f L b n₁ (S i) end)%ps.
imports: Utf8 QArith NPeano Sorting Misc Field2 Fpolynomial Fsummation Newton ConvexHull Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq F1Prop Q_field PosOrder QbarM