proposition: Theorem q_mj_mk_eq_p_h_j : ∀ f L j αj m mj p q, newton_segments f = Some L → pol_in_K_1_m f m → (Qnat j, αj) = ini_pt L → mj = mh_of_m m αj (ps_poly_nth j f) → p = p_of_m m (γ L) → q = Pos.to_nat (q_of_m m (γ L)) → ∀ h αh mh, (Qnat h, αh) ∈ oth_pts L ++ [fin_pt L] → mh = mh_of_m m αh (ps_poly_nth h f) → αh == mh # m ∧ (Z.of_nat q * (mj - mh) = p * Z.of_nat (h - j))%Z.
proof: Proof. intros f L j αj m mj p q HL Hm Hj Hmj Hp Hq h αh mh Hh Hmh. remember (points_of_ps_polynom f) as pts eqn:Hpts . remember (ps_poly_nth h f) as hps. apply List.in_app_or in Hh. remember HL as Hfin; clear HeqHfin. apply exists_fin_pt_nat in Hfin. destruct Hfin as (k, (αk, Hfin)). split. rewrite Hmh; simpl. unfold Qeq; simpl. unfold mh_of_m; simpl. subst hps. destruct Hh as [Hh| [Hk| ]]; [ idtac | idtac | contradiction ]. erewrite <- qden_αh_is_ps_polydo; eauto with Arith. rewrite Z_div_mul_swap. rewrite Z.div_mul; auto with Arith. eapply den_αh_divides_num_αh_m; eauto with Arith. erewrite <- qden_αk_is_ps_polydo; eauto with Arith. rewrite Z_div_mul_swap. rewrite Z.div_mul; auto with Arith. eapply den_αk_divides_num_αk_m; eauto with Arith. destruct Hh as [Hh| [Hh| ]]; [ idtac | idtac | contradiction ]. remember HL as Hgh; clear HeqHgh. eapply gamma_value_jh in Hgh; try eassumption. remember (q_of_m m (γ L)) as pq eqn:Hpq . pose proof (any_is_p_mq (γ L) m Hp Hpq) as H. destruct H as (Hgamma, Hg). rewrite Hgamma in Hgh. unfold Qnat in Hgh. rewrite <- Qnum_minus_distr_r in Hgh. rewrite Nat2Z.inj_sub. rewrite Hq. rewrite positive_nat_Z. eapply pmq_qmpm; try reflexivity. eapply j_lt_h; try eassumption; reflexivity. rewrite Hgh. remember Heqhps as Hhps; clear HeqHhps. eapply in_pts_in_pol in Hhps; try eassumption. destruct Hhps as (Hhps, Hαh). do 2 rewrite Qnum_minus_distr_r. eapply pol_ord_of_ini_pt in Hj; try eassumption; rewrite Hj. eapply pol_ord_of_oth_pt in Hh; try eassumption. rewrite Hh; reflexivity. subst hps; assumption. eapply oth_pts_in_init_pts; try eassumption. unfold newton_segments in HL. rewrite <- Hpts in HL; assumption. apply Nat.lt_le_incl. eapply j_lt_h; try eassumption; reflexivity. remember Hj as Hgh; clear HeqHgh. symmetry in Hh. eapply gamma_value_jk in Hgh; [ idtac | eassumption ]. remember (q_of_m m (γ L)) as pq eqn:Hpq . pose proof (any_is_p_mq (γ L) m Hp Hpq) as H. destruct H as (Hgamma, Hg). rewrite Hgh in Hgamma. unfold Qnat in Hgamma. rewrite <- Qnum_minus_distr_r in Hgamma. rewrite Nat2Z.inj_sub. rewrite Hq. rewrite positive_nat_Z. eapply pmq_qmpm; try reflexivity. eapply j_lt_k; try eassumption. rewrite <- Hj; simpl; rewrite nat_num_Qnat; reflexivity. rewrite <- Hh; simpl; rewrite nat_num_Qnat; reflexivity. rewrite <- Hgamma. remember Heqhps as Hhps; clear HeqHhps. eapply in_pts_in_pol with (hv := αh) in Hhps; try eassumption. destruct Hhps as (Hhps, Hαh). do 2 rewrite Qnum_minus_distr_r. eapply pol_ord_of_ini_pt in Hj; try eassumption; rewrite Hj. eapply pol_ord_of_fin_pt in Hh; try eassumption. rewrite Hh; reflexivity. subst hps; assumption. rewrite Hh. eapply ini_fin_ns_in_init_pts; try eassumption. unfold newton_segments in HL. rewrite <- Hpts in HL; assumption. apply Nat.lt_le_incl. eapply j_lt_k; try eassumption. rewrite <- Hj; simpl; rewrite nat_num_Qnat; reflexivity. rewrite <- Hh; simpl; rewrite nat_num_Qnat; reflexivity. Qed.
imports: Utf8 QArith Sorted NPeano ConvexHull ConvexHullMisc Misc NbarM QbarM Newton PolyConvexHull Field2 Fpolynomial PSpolynomial Puiseux_base Power_series Puiseux_series Ps_div Slope_base