proposition: Theorem αj_m_eq_p_r : ∀ f₁ L₁ αj₁ αk₁ m p₁ c₁ r, newton_segments f₁ = Some L₁ → pol_in_K_1_m f₁ m → ini_pt L₁ = (Qnat 0, αj₁) → fin_pt L₁ = (Qnat r, αk₁) → (0 < Qnum αj₁)%Z → Qnum αk₁ = 0%Z → c₁ = ac_root (Φq f₁ L₁) → root_multiplicity acf c₁ (Φq f₁ L₁) = r → p₁ = p_of_m m (γ L₁) → (Qnum αj₁ * Zpos m = p₁ * Z.of_nat r * Zpos (Qden αj₁))%Z.
proof: Proof. intros f₁ L₁ αj₁ αk₁ m p₁ c₁ r. intros HL₁ Hm Hini₁ Hfin₁ Hαj₁ Hαk₁ Hc₁ Hr₁ Hp₁. remember HL₁ as H; clear HeqH. eapply q_mj_mk_eq_p_h_j with (h := r) (αh := αk₁) in H; try eassumption; try reflexivity; try (symmetry; eassumption). rewrite Nat.sub_0_r in H. destruct H as (HH₂, HH₃). remember (q_of_m m (γ L₁)) as q₁. remember (mh_of_m m αj₁ (ps_poly_nth 0 f₁)) as mj'. remember (mh_of_m m αk₁ (ps_poly_nth r f₁)) as mk. unfold Qeq in HH₂; simpl in HH₂. rewrite Hαk₁ in HH₂; simpl in HH₂. symmetry in HH₂. apply Z.eq_mul_0_l in HH₂; [ | apply Pos2Z_ne_0 ]. move HH₂ at top; subst mk. rewrite Z.sub_0_r in HH₃. rewrite positive_nat_Z in HH₃. unfold mh_of_m in Heqmj'. unfold mh_of_m in Heqmj'. erewrite <- qden_αj_is_ps_polydo in Heqmj'; [ | eassumption | symmetry; eassumption ]. remember Heqq₁ as H; clear HeqH. eapply q_eq_1_any_r in H; try eassumption; [ | symmetry; assumption ]. rewrite H in HH₃. rewrite Z.mul_1_l in HH₃. rewrite <- HH₃. rewrite Heqmj'. symmetry. rewrite Z.mul_comm. rewrite <- Z.divide_div_mul_exact; [ | apply Pos2Z_ne_0 | ]. rewrite Z.mul_comm. rewrite Z.div_mul; [ apply eq_refl | apply Pos2Z_ne_0 ]. eapply den_αj_divides_num_αj_m; eassumption . apply List.in_or_app. right; left; eassumption . 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