proposition: Theorem order_āh_minus_ah_xαh_gt_αh : ∀ f L pl tl h āh ah αh, newton_segments f = Some L → pl = [ini_pt L … oth_pts L ++ [fin_pt L]] → tl = List.map (term_of_point f) pl → h ∈ List.map (λ t, power t) tl → āh = ps_poly_nth h f → ah = ps_monom (coeff_of_term R h tl) 0 → αh = ord_of_pt h pl → (order (āh - ah * ps_monom 1%K αh)%ps > qfin αh)%Qbar.
proof: Proof. intros f L pl tl h āh ah αh HL Hpl Htl Hh Hāh Hah Hαh. remember HL as Hval; clear HeqHval. eapply order_in_newton_segment with (h := h) (αh := αh) in Hval; eauto . rewrite <- Hāh in Hval. unfold order, Qbar.gt. remember (āh - ah * ps_monom 1%K αh)%ps as s eqn:Hs . remember (series_order (ps_terms s) 0) as n eqn:Hn . symmetry in Hn. destruct n as [n| ]; [ idtac | constructor ]. apply Qbar.qfin_lt_mono. unfold order in Hval. remember (series_order (ps_terms āh) 0) as m eqn:Hm . symmetry in Hm. destruct m as [m| ]; [ idtac | discriminate Hval ]. injection Hval; clear Hval; intros Hval. rewrite <- Hval. subst s; simpl. unfold cm; simpl. unfold cm; simpl. subst ah; simpl. unfold ps_ordnum_add; simpl. unfold cm, cm_factor; simpl. rewrite Z.mul_1_r. unfold Qlt; simpl. rewrite Pos2Z.inj_mul. rewrite Z.mul_assoc. rewrite Z.mul_shuffle0. apply Z.mul_lt_mono_pos_r; [ apply Pos2Z.is_pos | idtac ]. rewrite <- Hval; simpl. rewrite Z.mul_min_distr_nonneg_r; [ idtac | apply Pos2Z.is_nonneg ]. rewrite Z.min_l. rewrite Z.mul_add_distr_r. apply Z.add_lt_mono_l. rewrite <- positive_nat_Z, <- Nat2Z.inj_mul. apply Nat2Z.inj_lt. apply Nat.nle_gt; intros Hmn. apply series_order_iff in Hn. remember ps_add as g; simpl in Hn; subst g. destruct Hn as (Hni, Hn). remember (ps_monom (coeff_of_term R h tl) 0 * ps_monom 1%K αh)%ps as v. simpl in Hn. unfold cm, cm_factor in Hn; simpl in Hn. subst v; simpl in Hn. unfold cm in Hn; simpl in Hn. rewrite Z.mul_1_r in Hn. rewrite <- Hval in Hn; simpl in Hn. rewrite Z.min_l in Hn. rewrite Z.sub_diag in Hn; simpl in Hn. rewrite Nat.sub_0_r in Hn. rewrite Z.min_r in Hn. destruct (zerop (n mod Pos.to_nat (ps_polydo āh))) as [Hnp| Hnp]. apply Nat.mod_divides in Hnp; auto with Arith. destruct Hnp as (p, Hp). rewrite Nat.mul_comm in Hp. rewrite Hp in Hmn. apply Nat.mul_le_mono_pos_r in Hmn; [ idtac | apply Pos2Nat.is_pos ]. rewrite Hp in Hn. rewrite Nat.div_mul in Hn; auto with Arith; simpl in Hn. rewrite Z.mul_add_distr_r in Hn. rewrite Z.add_simpl_l in Hn. rewrite Z2Nat.inj_mul in Hn; simpl in Hn. rewrite Nat2Z.id in Hn. rewrite <- Hp in Hn. destruct (eq_nat_dec p m) as [Hpm| Hpm]. subst p. rewrite <- Hp, Nat.sub_diag in Hn. destruct (lt_dec n n) as [Hnn| Hnn]. revert Hnn; apply Nat.lt_irrefl. rewrite Nat.mod_0_l in Hn; auto with Arith; simpl in Hn. rewrite Nat.div_0_l in Hn; auto with Arith; simpl in Hn. unfold convol_mul in Hn. simpl in Hn. unfold summation in Hn; simpl in Hn. rewrite Nat.mod_0_l in Hn; auto with Arith; simpl in Hn. rewrite Nat.div_0_l in Hn; auto with Arith; simpl in Hn. rewrite rng_mul_1_r, rng_add_0_r in Hn. rewrite Htl in Hn. rewrite coeff_of_term_pt_eq in Hn. rewrite Hāh in Hn; simpl in Hn. unfold ps_poly_nth, ps_lap_nth in Hn; simpl in Hn. rewrite Hāh in Hm. unfold coeff_of_pt in Hn. rewrite coeff_of_hl_eq_order in Hn. unfold order_coeff in Hn. unfold ps_poly_nth, ps_lap_nth in Hm. rewrite Hm in Hn. rewrite rng_add_opp_r in Hn. apply Hn; reflexivity. subst tl; simpl in Hh. revert Hh; clear; intros. induction pl as [| (i, ai)]; [ assumption | simpl ]. simpl in Hh. destruct Hh as [Hh| Hh]; [ left; assumption | idtac ]. right; apply IHpl; assumption. destruct (lt_dec n (m * Pos.to_nat (ps_polydo āh))) as [Hnp| Hnp]. apply series_order_iff in Hm. destruct Hm as (Hmi, Hm). apply Nat_le_neq_lt in Hmn; [ idtac | assumption ]. apply Hmi in Hmn. rewrite rng_add_0_r in Hn; contradiction. apply Hnp. rewrite Hp. apply Nat.mul_lt_mono_pos_r; [ apply Pos2Nat.is_pos | idtac ]. apply Nat_le_neq_lt; assumption. apply Nat2Z.is_nonneg. apply Pos2Z.is_nonneg. rewrite rng_add_0_l in Hn. rewrite Z.mul_add_distr_r in Hn. rewrite Z.add_simpl_l in Hn. rewrite Z2Nat.inj_mul in Hn; simpl in Hn. rewrite Nat2Z.id in Hn. destruct (lt_dec n (m * Pos.to_nat (ps_polydo āh))) as [Hnm| Hnm]. apply Hn; reflexivity. apply Hnm; clear Hnm. destruct (eq_nat_dec n (m * Pos.to_nat (ps_polydo āh))) as [Heq| Hne]. rewrite Heq in Hnp. rewrite Nat.mod_mul in Hnp; auto with Arith. exfalso; revert Hnp; apply Nat.lt_irrefl. apply Nat_le_neq_lt; assumption. apply Nat2Z.is_nonneg. apply Pos2Z.is_nonneg. rewrite Z.mul_add_distr_r. apply Z.le_sub_le_add_l. rewrite Z.sub_diag, <- positive_nat_Z, <- Nat2Z.inj_mul. apply Nat2Z.is_nonneg. rewrite Z.mul_add_distr_r. apply Z.le_sub_le_add_l. rewrite Z.sub_diag, <- positive_nat_Z, <- Nat2Z.inj_mul. apply Nat2Z.is_nonneg. apply Z.le_sub_le_add_l. rewrite Z.sub_diag. apply Nat2Z.is_nonneg. rewrite Hαh. rewrite Htl in Hh; simpl in Hh. rewrite List.map_map in Hh. simpl in Hh. apply ord_is_ord_of_pt; [ idtac | idtac | assumption ]. rewrite Hpl. eapply ini_oth_fin_pts_sorted; eassumption. intros pt Hpt. eapply points_in_newton_segment_have_nat_abscissa; [ eassumption | idtac ]. subst pl; assumption. Qed.
imports: Utf8 QArith NPeano Sorted Misc NbarM QbarM SplitList Field2 Fpolynomial Fsummation Newton ConvexHull ConvexHullMisc PolyConvexHull Puiseux_base Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial AlgCloCharPol CharactPolyn F1Eq