proposition: Theorem q_is_factor_of_h_minus_j : ∀ f L j αj m q, newton_segments f = Some L → pol_in_K_1_m f m → (Qnat j, αj) = ini_pt L → q = Pos.to_nat (q_of_m m (γ L)) → ∀ h αh, (Qnat h, αh) ∈ oth_pts L ++ [fin_pt L] → (q | h - j)%nat.
proof: Proof. intros f L j αj m q HL Hm Hj Hq h αh Hh. remember (p_of_m m (γ L)) as p eqn:Hp . remember HL as H; clear HeqH. eapply q_mj_mk_eq_p_h_j in H; try eassumption; try reflexivity. destruct H as (Hαh, Hqjh). apply List.in_app_or in Hh. remember (q_of_m m (γ L)) as pq eqn:Hpq ; subst q. rename pq into q; rename Hpq into Hq. remember Hp as Hgcd; clear HeqHgcd. eapply p_and_q_have_no_common_factors in Hgcd; eauto with Arith. rewrite Z.gcd_comm in Hgcd. rewrite <- positive_nat_Z in Hgcd. rewrite Z.gcd_comm in Hgcd. rewrite Z.gcd_comm in Hgcd. apply Z.gauss with (p := Z.of_nat (h - j)) in Hgcd. destruct Hgcd as (c, Hc). exists (Z.to_nat c). apply Nat2Z.inj. rewrite Nat2Z.inj_mul. rewrite Z2Nat.id; [ assumption | idtac ]. eapply mul_pos_nonneg; try eassumption. destruct Hh as [Hh| [Hk| ]]; [ idtac | idtac | contradiction ]. eapply j_lt_h; try eassumption; reflexivity. eapply j_lt_k; try eassumption. rewrite <- Hj; simpl; rewrite nat_num_Qnat; reflexivity. rewrite Hk; simpl; rewrite nat_num_Qnat; reflexivity. rewrite <- Hqjh. apply Z.divide_factor_l. 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