proposition: Theorem next_pow_eq_p : ∀ f L c αj αk m r, newton_segments f = Some L → pol_in_K_1_m f m → c = ac_root (Φq f L) → root_multiplicity acf c (Φq f L) = r → ini_pt L = (Qnat 0, αj) → fin_pt L = (Qnat r, αk) → (0 < Qnum αj)%Z → Qnum αk = 0%Z → (0 < r)%nat → next_pow 0 L m = Z.to_nat (p_of_m m (γ L)).
proof: Proof. intros f L c αj αk m r HL Hm Hc Hr Hini Hfin Hαj Hαk Hrp. unfold next_pow; simpl. rewrite Hini, Hfin; simpl. rewrite Hαk; simpl. rewrite Qnum_inv_Qnat_sub; [ | assumption ]. rewrite Qden_inv_Qnat_sub; [ | assumption ]. rewrite Z.add_0_r, Z.mul_1_r, Nat.sub_0_r, Pos.mul_1_r. rewrite Z.mul_shuffle0, Pos_mul_shuffle0. rewrite Pos2Z.inj_mul. rewrite Z.div_mul_cancel_r; try apply Pos2Z_ne_0. erewrite αj_m_eq_p_r with (f₁ := f); try eassumption; [ | reflexivity ]. rewrite Pos.mul_comm. rewrite Pos2Z.inj_mul, Zposnat2Znat; [ | assumption ]. rewrite <- Z.mul_assoc. rewrite Z.div_mul; [ reflexivity | ]. rewrite <- Zposnat2Znat; [ | assumption ]. apply Pos2Z_ne_0. 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