proposition: Theorem order_āl_xlγ₁_gt_β₁ : ∀ f L pl tl l₁ l₂ l āl, newton_segments f = Some L → pl = [ini_pt L … oth_pts L ++ [fin_pt L]] → tl = List.map (term_of_point f) pl → l₁ = List.map (λ t, power t) tl → split_list (List.seq 0 (length (al f))) l₁ l₂ → l ∈ l₂ → āl = ps_poly_nth l f → (order (āl * ps_monom 1%K (Qnat l * γ L))%ps > qfin (β L))%Qbar.
proof: Proof. intros f L pl tl l₁ l₂ l āl HL Hpl Htl Hl₁ Hsl Hl Hāl. remember (āl * ps_monom 1%K (Qnat l * γ L))%ps as s eqn:Hs . remember (series_order (ps_terms s) 0) as n eqn:Hn . symmetry in Hn. destruct n as [n| ]. remember (points_of_ps_polynom f) as pts eqn:Hpts . remember Hpts as Hval; clear HeqHval. remember (order āl) as m eqn:Hm . symmetry in Hm. destruct m as [m| ]. eapply in_pol_in_pts in Hval; try eassumption. remember HL as H; clear HeqH. eapply points_not_in_any_newton_segment with (αh := m) (h := Qnat l) in H; try eassumption. unfold order, Qbar.gt. rewrite Hn. apply Qbar.qfin_lt_mono. remember (β L) as βL. remember (γ L) as γL. rewrite Hs, Hāl; simpl. unfold cm; simpl. rewrite <- Hāl. eapply Qlt_le_trans; [ eassumption | idtac ]. unfold Qle; simpl. do 2 rewrite Pos2Z.inj_mul. do 2 rewrite Z.mul_assoc. apply Z.mul_le_mono_pos_r; [ apply Pos2Z.is_pos | idtac ]. do 3 rewrite Z.mul_add_distr_r. rewrite Z.add_shuffle0. apply Z.add_le_mono. unfold order in Hm. remember (series_order (ps_terms āl) 0) as p eqn:Hp . symmetry in Hp. destruct p as [p| ]; [ idtac | discriminate Hm ]. injection Hm; clear Hm; intros Hm. rewrite <- Hm; simpl. do 2 rewrite Z.mul_add_distr_r. apply Z.add_le_mono_l. apply Z.mul_le_mono_pos_r; [ apply Pos2Z.is_pos | idtac ]. rewrite <- positive_nat_Z. rewrite <- Nat2Z.inj_mul. apply Nat2Z.inj_le. rewrite Hs in Hn; simpl in Hn. unfold cm_factor in Hn; simpl in Hn. apply series_order_iff in Hn; simpl in Hn. apply series_order_iff in Hp; simpl in Hp. destruct Hn as (Hni, Hn). destruct Hp as (Hpi, Hp). unfold convol_mul in Hn. rewrite summation_only_one_non_0 with (v := n) in Hn. rewrite Nat.sub_diag 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 in Hn. destruct (zerop (n mod Pos.to_nat (Qden (γL)))) as [Hng| Hng]. apply Nat.mod_divides in Hng; auto with Arith. destruct Hng as (g, Hg). rewrite Hg, Nat.mul_comm. apply Nat.mul_le_mono_l. rewrite Hg in Hn. rewrite Nat.mul_comm in Hn. rewrite Nat.div_mul in Hn; auto with Arith. apply Nat.nlt_ge. clear H; intros H. apply Hpi in H. contradiction. exfalso; apply Hn; reflexivity. split; [ apply Nat.le_0_l | reflexivity ]. intros i (_, Hin) Hinn. apply rng_mul_eq_0. right. unfold series_stretch; simpl. destruct (zerop ((n - i) mod Pos.to_nat (ps_polydo āl))) as [Hz| Hz]. apply Nat.mod_divides in Hz; auto with Arith. destruct Hz as (c, Hc). rewrite Nat.mul_comm in Hc; rewrite Hc. rewrite Nat.div_mul; auto with Arith. destruct c; [ idtac | reflexivity ]. rewrite Nat.mul_0_l in Hc. apply Nat.sub_0_le in Hc. exfalso; apply Hinn, Nat.le_antisymm; auto with Arith. reflexivity. rewrite Z.mul_shuffle0; reflexivity. split; [ eassumption | idtac ]. intros Hlm. apply split_list_comm in Hsl. eapply sorted_split_in_not_in in Hsl; try eassumption. apply Hsl; clear Hsl. subst l₁ tl pl. rewrite List.map_map; simpl. destruct Hlm as [Hlm| Hlm]. left; rewrite Hlm; simpl. rewrite nat_num_Qnat; reflexivity. right. rewrite List.map_app; simpl. apply List.in_or_app. destruct Hlm as [Hlm| Hlm]. right; rewrite Hlm. left; simpl; rewrite nat_num_Qnat; reflexivity. left. revert Hlm; clear; intros. remember (oth_pts L) as pts; clear Heqpts. induction pts as [| (i, ai)]; [ contradiction | idtac ]. destruct Hlm as [Hlm| Hlm]. injection Hlm; clear Hlm; intros; subst; simpl. left; rewrite nat_num_Qnat; reflexivity. right; apply IHpts, Hlm. remember (length (al f)) as len; clear. remember 0%nat as b; clear Heqb. revert b. induction len; intros; [ constructor | simpl ]. constructor; [ apply IHlen | idtac ]. destruct len; constructor. apply Nat.lt_succ_diag_r. unfold order in Hm. remember (series_order (ps_terms āl) 0) as v eqn:Hv . symmetry in Hv. destruct v; [ discriminate Hm | idtac ]. apply ps_series_order_inf_iff in Hv. assert (s = 0)%ps as Hsz. rewrite Hs. rewrite Hv. rewrite ps_mul_0_l; reflexivity. apply order_inf in Hsz. rewrite Hsz; constructor. unfold order; simpl. rewrite Hn; constructor. 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