proposition: Theorem q_eq_1_any_r : ∀ f L c αj αk m q r, newton_segments f = Some L → pol_in_K_1_m f m → q = q_of_m m (γ L) → c = ac_root (Φq f L) → r = root_multiplicity acf c (Φq f L) → ini_pt L = (Qnat 0, αj) → fin_pt L = (Qnat r, αk) → (0 < Qnum αj)%Z → Qnum αk = 0%Z → q = 1%positive.
proof: Proof. intros f L c αj αk m q r HL Hm Hq Hc Hr Hini Hfin Hαj Hαk. remember Hr as Hrv; clear HeqHrv. remember (al (Φq f L)) as cf eqn:Hcf . remember Hcf as H; clear HeqH. rewrite al_Φq in H. remember [ini_pt L … oth_pts L ++ [fin_pt L]] as pl eqn:Hpl . remember (List.map (term_of_point f) pl) as tl eqn:Htl . rewrite Hini in H. simpl in H. rewrite nat_num_Qnat in H; simpl in H. subst cf. rename H into Hcf. unfold root_multiplicity in Hr. rewrite Hcf in Hr. erewrite length_char_pol in Hr; try eassumption. rewrite <- Hcf in Hr. rewrite Nat.sub_0_r in Hr. remember Hrv as H; clear HeqH. eapply phi_zq_eq_z_sub_c₁_psi in H; [ | reflexivity ]. unfold eq_poly in H. rewrite Hcf in H. remember quotient_phi_x_sub_c_pow_r as g; simpl in H; subst g. remember (quotient_phi_x_sub_c_pow_r (Φq f L) c r) as Ψ. eapply Ψ_length in HeqΨ; try eassumption. rewrite Nat.sub_0_r, Nat_sub_succ_diag in HeqΨ. rename H into Hcp. 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; [ | symmetry; eassumption | ]. rewrite <- Hq, Nat.sub_0_r in H. remember (mh_of_m m αj (ps_poly_nth 0 f)) as mj eqn:Hmj . eapply pol_ord_of_ini_pt in Hmj; try eassumption; [ | symmetry; assumption ]. remember (mh_of_m m αk (ps_poly_nth r f)) as mk eqn:Hmk . eapply pol_ord_of_fin_pt in Hmk; try eassumption; [ | symmetry; assumption ]. destruct H as (_, Hqjr). unfold Qeq in Hmk. simpl in Hmk. rewrite Hαk in Hmk. simpl in Hmk. symmetry in Hmk. apply Z.mul_eq_0_l in Hmk; [ | apply Pos2Z_ne_0 ]. subst mk. rewrite Z.sub_0_r in Hqjr. rewrite positive_nat_Z in Hqjr. remember (p_of_m m (γ L)) as p eqn:Hp . move Hp after Hq. remember HL as H; clear HeqH. eapply phi_degree_is_k_sub_j_div_q in H; try (symmetry; eassumption); [ | eassumption | reflexivity ]. unfold Φs in H. rewrite Nat.sub_0_r, <- Hq in H. unfold has_degree in H. unfold pseudo_degree in H. remember (al (poly_shrink (Pos.to_nat q) (Φq f L))) as psh eqn:Hpsh . unfold poly_shrink in Hpsh. rewrite Hcf in Hpsh. simpl in Hpsh. destruct H as (Hshr, (Hdeg, Hpdeg)). remember (Pos.to_nat q) as nq eqn:Hnq . symmetry in Hnq. destruct nq; [ exfalso; revert Hnq; apply Pos2Nat_ne_0 | ]. destruct nq; [ apply Pos2Nat.inj; assumption | exfalso ]. unfold poly_shrinkable in Hshr. rewrite Hcf in Hshr. assert (H : (1 mod S (S nq) ≠ 0)%nat). rewrite Nat.mod_1_l; [ intros H; discriminate H | ]. apply lt_n_S, Nat.lt_0_succ. apply Hshr in H. remember (al Ψ) as la eqn:Hla . symmetry in Hla. destruct la as [| a]; [ discriminate HeqΨ | ]. destruct la; [ | discriminate HeqΨ ]. destruct (fld_zerop a) as [H₁| H₁]. rewrite H₁ in Hcp. rewrite lap_eq_0 in Hcp. rewrite lap_mul_nil_r in Hcp. rewrite Htl, Hpl in Hcp. simpl in Hcp. rewrite Hini in Hcp; simpl in Hcp. apply lap_eq_cons_nil_inv in Hcp. rewrite nat_num_Qnat in Hcp. destruct Hcp as (Hoj, Hcp). revert Hoj. eapply ord_coeff_non_zero_in_newt_segm; [ eassumption | | reflexivity ]. left; eassumption. rewrite lap_mul_comm in Hcp. rewrite binomial_expansion in Hcp. rewrite lap_mul_const_l in Hcp. rewrite List.map_map in Hcp. assert (HH : (List.nth 1 (make_char_pol R 0 tl) 0 = 0)%K). rewrite H; reflexivity. rewrite list_nth_rng_eq in HH; [ | eassumption ]. simpl in HH. destruct r. symmetry in Hrv. revert Hrv; apply multiplicity_neq_0; assumption. simpl in HH. unfold nth_coeff in HH. simpl in HH. rewrite comb_0_r, comb_1_r in HH. rewrite Nat.add_1_l in HH. rewrite Nat.sub_0_r in HH. apply fld_eq_mul_0_r in HH; try assumption. rewrite <- rng_mul_1_l in HH. rewrite rng_mul_comm in HH. rewrite rng_mul_nat_assoc in HH. rewrite rng_mul_comm in HH. rewrite <- rng_mul_nat_assoc in HH. apply fld_eq_mul_0_r in HH; [ | assumption | ]. clear H. remember HL as H; clear HeqH. eapply char_pol_root_ne_0 with (m := m) (c₁ := c) in H; try eassumption. apply H. apply rng_opp_inj_wd. rewrite rng_opp_0. remember r as n in HH. clear Heqn. destruct (fld_zerop 1%K) as [H₀| H₀]. etransitivity; [ apply eq_1_0_all_0; assumption | ]. symmetry; apply eq_1_0_all_0; assumption. induction n; [ contradiction | ]. simpl in HH. apply fld_eq_mul_0_r in HH; [ apply IHn, HH | assumption | ]. intros I. apply rng_opp_inj_wd in I. apply H. rewrite rng_opp_0 in I. rewrite <- I. apply rng_add_move_0_r. apply rng_add_opp_r. destruct (fld_zerop 1%K) as [H₀| H₀]. exfalso; apply H₁; apply eq_1_0_all_0; assumption. destruct r; [ simpl; rewrite rng_add_0_l; assumption | ]. apply ac_charac_01. apply List.in_or_app; right; left; assumption. 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