proposition: Theorem each_power_of_y₁_in_g_has_coeff_pos_ord : ∀ f L g, newton_segments f = Some L → g = g_of_ns f L → ∀ m, m ∈ al g → (order m > 0)%Qbar.
proof: Proof. intros f L g HL Hg m Hm. remember (al g) as la eqn:Hla . subst g. unfold g_of_ns, g_lap_of_ns in Hla. remember (ac_root (Φq f L)) as c₁ eqn:Hc₁ . 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 . remember (List.map (λ t, power t) tl) as l₁ eqn:Hl₁ . remember (list_seq_except 0 (length (al f)) l₁) as l₂ eqn:Hl₂ . simpl in Hla. remember (order m) as om eqn:Hom . symmetry in Hom. destruct om as [om| ]; [ idtac | constructor ]. assert (m ≠ 0)%ps as Hmnz. intros H. apply order_inf in H. rewrite H in Hom; discriminate Hom. subst la. apply list_in_ps_lap_in in Hm; [ idtac | assumption ]. progress unfold ps_lap_add in Hm. progress unfold ps_lap_mul in Hm. rewrite lap_mul_add_distr_l in Hm. rewrite <- Hom. apply ps_lap_in_add in Hm; [ assumption | idtac | idtac ]. clear m om Hom Hmnz Hm. intros m Hm. progress unfold ps_lap_summ in Hm. rewrite lap_mul_summation in Hm. eapply ps_lap_in_summation; [ idtac | eassumption ]. clear m Hm. intros h Hh m Hm. simpl in Hm. rewrite lap_mul_assoc in Hm. apply ps_lap_in_mul in Hm; [ assumption | idtac | idtac ]. clear m Hm. intros m Hm. remember (ps_poly_nth h f) as āh eqn:Hāh . remember (ps_monom (coeff_of_term R h tl) 0) as ah eqn:Hah . remember (ord_of_pt h pl) as αh eqn:Hαh . rewrite lap_mul_const_l in Hm; simpl in Hm. destruct Hm as [(Hmnz, Hm)| ]; [ idtac | contradiction ]. rewrite <- Hm; simpl. rewrite order_mul. remember (āh - ah * ps_monom 1%K αh)%ps as aa. remember (ps_monom 1%K (Qnat h * γ L))%ps as bb. remember (ps_monom 1%K (- β L)) as cc. remember (order (aa * bb)) as oaa. apply Qbar.lt_le_trans with (m := (qfin (- β L) + oaa)%Qbar). subst oaa. rewrite order_mul. rewrite Qbar.add_comm. rewrite Heqaa, Heqbb. apply Qbar.le_lt_trans with (m := qfin (αh + Qnat h * γ L - β L)). apply Qbar.le_qfin. apply Qplus_le_l with (z := β L). rewrite <- Qminus_minus_assoc. rewrite Qminus_diag. rewrite Qplus_0_l. unfold Qminus, Qopp; simpl. rewrite Qplus_0_r. remember (points_of_ps_polynom f) as pts. eapply points_in_convex; try eassumption. eapply in_pol_in_pts; try eassumption. rewrite Hāh. eapply order_in_newton_segment; try eassumption. rewrite Hαh. apply ord_is_ord_of_pt. rewrite Hpl. eapply ini_oth_fin_pts_sorted; eassumption. intros pt Hpt. rewrite Hpl in Hpt. eapply points_in_newton_segment_have_nat_abscissa; eassumption. rewrite Hl₁, Htl in Hh. rewrite List.map_map in Hh; assumption. unfold Qminus. rewrite Qbar.qfin_inj_add. apply Qbar.add_lt_mono_r; [ intros H; discriminate H | idtac ]. rewrite Qbar.qfin_inj_add. apply Qbar.add_lt_le_mono; [ intros H; discriminate H | idtac | idtac ]. rewrite Hl₁ in Hh. eapply order_āh_minus_ah_xαh_gt_αh; eassumption. apply ps_monom_order_ge. destruct oaa as [oaa| ]. apply Qbar.add_le_mono_r; [ intros H; discriminate H | idtac ]. subst cc; apply ps_monom_order_ge. simpl. rewrite Qbar.add_comm; constructor. clear m Hm. intros m Hm. eapply ps_lap_in_power; [ idtac | eassumption ]. clear m Hm. intros m Hm. simpl in Hm. destruct Hm as [(Hn, Hm)| Hm]. rewrite <- Hm. apply ps_monom_order_ge. destruct Hm as [(Hn, Hm)| ]; [ idtac | contradiction ]. rewrite <- Hm. apply ps_monom_order_ge. clear m om Hom Hmnz Hm. intros m Hm. progress unfold ps_lap_summ in Hm. rewrite lap_mul_summation in Hm. eapply ps_lap_in_summation; [ idtac | eassumption ]. clear m Hm. intros h Hh m Hm. simpl in Hm. rewrite lap_mul_assoc in Hm. apply ps_lap_in_mul in Hm; [ assumption | idtac | idtac ]. clear m Hm. intros m Hm. simpl in Hm. destruct Hm as [(H₁, H₂)| Hm]; [ idtac | contradiction ]. unfold summation in H₁, H₂; simpl in H₁, H₂. rewrite ps_add_0_r in H₂. rewrite <- H₂. rewrite order_mul. remember (ps_poly_nth h f) as āh. apply Qbar.lt_sub_lt_add_l; [ intros H; discriminate H | idtac ]. rewrite Qbar.sub_0_l. destruct (fld_zerop 1%K) as [Hoz| Honz]. rewrite ps_monom_0_order; [ simpl | assumption ]. rewrite order_mul. rewrite ps_monom_0_order; [ simpl | assumption ]. rewrite Qbar.add_comm; constructor. rewrite ps_monom_order; [ simpl | assumption ]. rewrite Qopp_opp. eapply order_āl_xlγ₁_gt_β₁; try eassumption. apply except_split_seq; [ idtac | idtac | assumption ]. subst l₁ tl. rewrite List.map_map; simpl. apply Sorted_map; simpl. remember HL as Hsort; clear HeqHsort. apply ini_oth_fin_pts_sorted in Hsort. rewrite <- Hpl in Hsort. pose proof (points_in_newton_segment_have_nat_abscissa K f HL) as Hnat. rewrite <- Hpl in Hnat. revert Hsort Hnat; clear; intros. induction pl as [| p]; [ constructor | idtac ]. apply Sorted_inv in Hsort. destruct Hsort as (Hsort, Hrel). constructor. apply IHpl; [ assumption | idtac ]. intros pt Hpt. apply Hnat; right; assumption. revert Hrel Hnat; clear; intros. induction pl as [| q]; constructor. apply HdRel_inv in Hrel. unfold fst_lt in Hrel; simpl. unfold nat_num; simpl. assert (p ∈ [p; q … pl]) as Hp by (left; reflexivity). assert (q ∈ [p; q … pl]) as Hq by (right; left; reflexivity). apply Hnat in Hp. apply Hnat in Hq. destruct Hp as (h, (αh, Hp)). destruct Hq as (i, (αi, Hq)). subst p q; simpl in Hrel; simpl. do 2 rewrite Nat2Z.id. apply Qnat_lt; assumption. subst l₁; simpl. apply List.Forall_forall; intros i Hi. split; [ apply Nat.le_0_l | idtac ]. subst tl; simpl in Hi. rewrite List.map_map in Hi. simpl in Hi. revert HL Hpl Hi; clear; intros. apply ord_is_ord_of_pt in Hi. rewrite Hpl in Hi at 2. unfold newton_segments in HL. eapply ns_in_init_pts in Hi; [ idtac | eassumption ]. eapply in_pts_in_pol with (def := 0%ps) in Hi; try reflexivity. destruct Hi as (Hi, Ho). apply Nat.nle_gt. intros H. apply List.nth_overflow with (d := 0%ps) in H. rewrite H in Ho. rewrite order_0 in Ho. discriminate Ho. rewrite Hpl. eapply ini_oth_fin_pts_sorted; eassumption. intros pt Hpt. subst pl. eapply points_in_newton_segment_have_nat_abscissa; eassumption. clear m Hm. intros m Hm. eapply ps_lap_in_power; [ idtac | eassumption ]. intros a Ha. simpl in Ha. destruct Ha as [(Hn, Ha)| Ha]. rewrite <- Ha. apply ps_monom_order_ge. destruct Ha as [(_, Ha)| Ha]; [ idtac | contradiction ]. rewrite <- Ha; simpl. apply ps_monom_order_ge. 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