proposition: Theorem length_char_pol : ∀ f L pl tl j αj k αk, newton_segments f = Some L → ini_pt L = (Qnat j, αj) → fin_pt L = (Qnat k, αk) → pl = [ini_pt L … oth_pts L ++ [fin_pt L]] → tl = List.map (term_of_point f) pl → length (make_char_pol R j tl) = S (k - j).
proof: Proof. intros f L pl tl j αj k αk HL Hini Hfin Hpl Htl. rewrite Htl, Hpl, Hini; simpl. rewrite nat_num_Qnat, Nat.sub_diag; simpl. rewrite List.map_app; simpl. rewrite length_char_pol_succ; simpl. rewrite Hfin; simpl. rewrite nat_num_Qnat. reflexivity. remember (List.map (term_of_point f) (oth_pts L)) as tl₂ eqn:Htl₂ . remember (term_of_point f (Z.of_nat k # 1, αk)) as tk eqn:Htk . unfold term_of_point, lap_term_of_point in Htk; simpl in Htk. unfold nat_num in Htk; simpl in Htk. rewrite Nat2Z.id in Htk. subst tk; simpl. remember (oth_pts L) as pts eqn:Hpts . symmetry in Hpts. destruct pts as [| (h, αh)]. subst tl₂; simpl. rewrite Hfin; simpl; rewrite nat_num_Qnat; eapply j_lt_k; try eassumption. rewrite Hini; simpl; rewrite nat_num_Qnat; reflexivity. rewrite Hfin; simpl; rewrite nat_num_Qnat; reflexivity. subst tl₂; simpl. assert ((h, αh) ∈ oth_pts L) as Hh by (rewrite Hpts; left; reflexivity). remember Hh as H; clear HeqH. eapply exists_oth_pt_nat in H; [ idtac | eassumption ]. destruct H as (i, (ai, Hi)). injection Hi; clear Hi; intros; subst h ai; rename i into h. rewrite nat_num_Qnat. symmetry in Hini. eapply j_lt_h; try eassumption; reflexivity. remember HL as Hsort; clear HeqHsort. apply ini_oth_fin_pts_sorted in Hsort. apply Sorted_inv_1 in Hsort. remember (oth_pts L ++ [fin_pt L]) as pts eqn:Hpts . remember (List.map (term_of_point f) pts) as li eqn:Hli . remember Hli as H; clear HeqH. rewrite Hpts in Hli. rewrite List.map_app in Hli; simpl in Hli. rewrite <- Hli, H. assert (∀ pt, pt ∈ pts → ∃ (h : nat) (αh : Q), pt = (Qnat h, αh)) as Hnat. intros pt Hpt. eapply points_in_newton_segment_have_nat_abscissa; try eassumption. right; rewrite <- Hpts; assumption. revert Hsort Hnat; clear; intros. induction pts as [| pt]; [ constructor | simpl ]. constructor. apply IHpts. eapply Sorted_inv_1; eassumption. intros pt₁ Hpt₁. apply Hnat. right; assumption. apply Sorted_inv in Hsort. destruct Hsort as (_, Hrel). unfold fst_lt in Hrel. revert Hrel Hnat; clear; intros. destruct pts as [| pt₁]; constructor; simpl. apply HdRel_inv in Hrel. assert (pt ∈ [pt; pt₁ … pts]) as H₁ by (left; reflexivity). assert (pt₁ ∈ [pt; pt₁ … pts]) as H₂ by (right; left; reflexivity). apply Hnat in H₁. apply Hnat in H₂. destruct H₁ as (h₁, (ah₁, Hh₁)). destruct H₂ as (h₂, (ah₂, Hh₂)). subst pt pt₁; simpl in Hrel; simpl. do 2 rewrite nat_num_Qnat. apply Qnat_lt; 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