proposition: Theorem f₁_in_K_1_mq₀ : ∀ f L f₁ m, pol_in_K_1_m f m → newton_segments f = Some L → f₁ = next_pol f (β L) (γ L) (ac_root (Φq f L)) → pol_in_K_1_m f₁ (m * q_of_m m (γ L)).
proof: Proof. intros f L f₁ m Hm HL Hf₁. eapply next_pol_in_K_1_mq in HL; try eassumption; reflexivity. Qed.
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