fact: Definition f₁_root_when_r_constant f L := if fld_zerop 1%K then 0%ps else let m := ps_pol_com_polydo f in let q₀ := q_of_m m (γ L) in let f₁ := next_pol f (β L) (γ L) (ac_root (Φq f L)) in let L₁ := option_get phony_ns (newton_segments f₁) in let s := root_tail (m * q₀) 0 f₁ L₁ in match order (ps_pol_apply f₁ s) with | qfin ofs => let N := Z.to_nat (2 * Zpos m * Zpos q₀ * Qnum ofs) in if zerop_1st_n_const_coeff N f₁ L₁ then match lowest_with_zero_1st_const_coeff acf N f₁ L₁ with | O => 0%ps | S i' => root_head 0 i' f₁ L₁ end else 0%ps | ∞%Qbar => s end.
imports: Utf8 QArith NPeano Sorting Misc SlopeMisc Slope_base QbarM NbarM Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull PolyConvexHull NotInSegment Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq PosOrder F1Prop InK1m Q_field RootHeadTail RootAnyR