proposition: Theorem order_in_newton_segment : ∀ f L pl h αh, newton_segments f = Some L → pl = [ini_pt L … oth_pts L ++ [fin_pt L]] → (Qnat h, αh) ∈ pl → order (ps_poly_nth h f) = qfin αh.
proof: Proof. intros f L pl h αh HL Hpl Hαh. remember HL as Hini; clear HeqHini. apply exists_ini_pt_nat in Hini. destruct Hini as (j, (αj, Hini)). remember HL as Hfin; clear HeqHfin. apply exists_fin_pt_nat in Hfin. destruct Hfin as (k, (αk, Hfin)). unfold ps_poly_nth, ps_lap_nth; simpl. edestruct in_pts_in_pol; try reflexivity; try eassumption. subst pl. simpl in Hαh. destruct Hαh as [Hαh| Hαh]. rewrite Hini in Hαh. injection Hαh; clear Hαh; intros HH H; subst αh. apply Nat2Z.inj in H; subst h. rewrite <- Hini. apply ini_fin_ns_in_init_pts; assumption. apply List.in_app_or in Hαh. destruct Hαh as [Hαh| Hαh]. eapply oth_pts_in_init_pts; try reflexivity; try eassumption. destruct Hαh as [Hαh| Hαh]; [ idtac | contradiction ]. rewrite Hfin in Hαh. injection Hαh; clear Hαh; intros HH H; subst αh. apply Nat2Z.inj in H; subst h. rewrite <- Hfin. apply ini_fin_ns_in_init_pts; assumption. 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