fact: Definition next_pow pow L₁ m := let n := (γ L₁ * inject_Z (Zpos m)) in (pow + Z.to_nat (Qnum n / Zpos (Qden n)))%nat.
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