proposition: Theorem fold_right_exists : ∀ f L pts j k αj αk g la, newton_segments f = Some L → pts = [ini_pt L … oth_pts L ++ [fin_pt L]] → ini_pt L = (Qnat j, αj) → fin_pt L = (Qnat k, αk) → (∀ i a b, ps_lap_eq a b → ps_lap_eq (g i a) (g i b)) → ps_lap_eq (List.fold_right g la (List.map (λ pt, nat_num (fst pt)) pts)) (List.fold_right (λ i accu, if List.existsb (λ pt, Nat.eqb i (nat_num (fst pt))) pts then g i accu else accu) la (List.seq j (S (k - j)))).
proof: Proof. intros f L pts j k αj αk g la HL Hpl Hini Hfin Hi. assert (j < k)%nat as Hjk. eapply j_lt_k; try eassumption. rewrite Hini; simpl; rewrite nat_num_Qnat; reflexivity. rewrite Hfin; simpl; rewrite nat_num_Qnat; reflexivity. subst pts; simpl. rewrite Hini; simpl. rewrite nat_num_Qnat; simpl. rewrite Nat.eqb_refl; simpl. apply Hi. remember HL as Hsort; clear HeqHsort. apply ini_oth_fin_pts_sorted in Hsort. remember (oth_pts L ++ [fin_pt L]) as pts eqn:Hpts . assert (∀ i αi, (Qnat i, αi) ∈ pts → (j < i)%nat) as Hjh. intros h αh H. symmetry in Hini. rewrite Hpts in H. apply List.in_app_or in H. destruct H as [H| H]. eapply j_lt_h; try eassumption; reflexivity. destruct H as [H| H]; [ idtac | contradiction ]. rewrite Hfin in H. injection H; clear H; intros _ H. apply Nat2Z.inj in H. subst h; assumption. assert (∀ iq αi, (iq, αi) ∈ pts → ∃ i, iq = Qnat i) as Hnat. intros iq αi Hip. eapply L_nat; [ eassumption | reflexivity | idtac ]. right; subst pts; eassumption. rewrite Hini in Hsort; clear Hini. rewrite Hfin in Hpts; clear Hfin. assert (List.last pts (0, 0) = (Qnat k, αk)) as Hlast. subst pts; simpl. clear; induction (oth_pts L) as [| x l]; [ reflexivity | simpl ]. destruct l as [| y]; [ reflexivity | simpl in IHl; simpl ]. assumption. rewrite fold_right_eqb_or; [ idtac | apply Nat.lt_succ_r; reflexivity ]. revert Hi Hjk Hjh Hnat Hlast Hsort; clear; intros. revert j k αj αk la Hjk Hjh Hlast Hsort. induction pts as [| (h, αh)]; intros. simpl in Hlast. injection Hlast; clear; intros; subst. rewrite <- Nat2Z.inj_0 in H0. progress unfold ps_lap_eq. apply Nat2Z.inj in H0; subst k; reflexivity. simpl. assert ((h, αh) ∈ [(h, αh) … pts]) as Hh by (left; reflexivity). apply Hnat in Hh. destruct Hh as (i, Hh). subst h; rename i into h. rewrite nat_num_Qnat. destruct (eq_nat_dec h k) as [H₁| H₁]. subst h. pose proof (le_n_Sn k) as H. apply Nat.sub_le_mono_r with (p := S j) in H. rewrite list_seq_app with (dj := (k - S j)%nat); auto with Arith; clear H. rewrite List.fold_right_app; simpl. rewrite <- Nat.add_succ_r, <- Nat.sub_succ_l; auto with Arith; simpl. rewrite Nat.add_sub_assoc; [ idtac | apply Nat.lt_le_incl; auto ]. rewrite Nat.add_comm, Nat.add_sub. rewrite Nat_sub_sub_distr; auto with Arith; rewrite Nat.add_succ_r. rewrite Nat.sub_add; [ idtac | apply Nat.lt_le_incl; auto ]. rewrite Nat_sub_succ_diag; simpl. rewrite Nat.eqb_refl; simpl. simpl in Hlast. destruct pts as [| pt]; [ simpl | exfalso ]. progress unfold ps_lap_eq. rewrite fold_nothing; [ reflexivity | idtac ]. intros i Hji Hij. rewrite orb_false_r. apply Nat.eqb_neq. intros H; subst i. rewrite Nat.add_sub_assoc in Hij; auto with Arith. rewrite Nat.add_comm, Nat.add_sub in Hij. revert Hij; apply Nat.lt_irrefl. revert Hsort Hlast Hnat; clear; intros. apply Sorted_inv_1 in Hsort. revert pt Hsort Hlast Hnat. induction pts as [| pt₂]; intros. simpl in Hlast. subst pt. apply Sorted_inv in Hsort. destruct Hsort as (_, Hrel). progress unfold fst_lt in Hrel; apply HdRel_inv in Hrel. simpl in Hrel. revert Hrel; apply Qlt_irrefl. apply IHpts with (pt := pt₂). eapply Sorted_minus_2nd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Qlt_trans; eassumption. assumption. intros iq αi Hpti. apply Hnat with (αi := αi). destruct Hpti as [H| H]; [ rewrite H; left; reflexivity | idtac ]. right; right; assumption. assert (h < k)%nat as Hhk. apply Sorted_inv_1 in Hsort. clear Hjk. clear IHpts. revert h k αh αk Hsort Hlast Hnat Hjh H₁. induction pts as [| (l, al)]; intros. injection Hlast; clear Hlast; intros HH H. exfalso; apply H₁, Nat2Z.inj; assumption. assert ((l, al) ∈ [(Qnat h, αh); (l, al) … pts]) as Hl by (right; left; reflexivity). apply Hnat in Hl. destruct Hl as (m, Hl); subst l; rename m into l. apply Nat.lt_le_trans with (m := l). apply Sorted_inv in Hsort. destruct Hsort as (_, Hrel). apply HdRel_inv in Hrel. progress unfold fst_lt in Hrel; simpl in Hrel. apply Qnat_lt; assumption. destruct (eq_nat_dec l k) as [H₂| H₂]. subst l; reflexivity. apply Sorted_inv_1 in Hsort. remember [(Qnat l, al) … pts] as p; simpl in Hlast; subst p. apply Nat.lt_le_incl. eapply IHpts; try eassumption. intros; apply Hnat with (αi := αi); right; assumption. intros; apply Hjh with (αi := αi); right; assumption. remember Hhk as H; clear HeqH. apply Nat.lt_le_incl in H. apply Nat.sub_le_mono_r with (p := S j) in H. apply Nat.le_le_succ_r in H. rewrite <- Nat.sub_succ_l in H; auto with Arith; simpl in H. rewrite list_seq_app with (dj := (h - S j)%nat); auto with Arith. assert (j < h)%nat as Hjh₁. apply Hjh with (αi := αh); left; reflexivity. rewrite Nat.add_sub_assoc; auto with Arith; clear H. rewrite Nat.add_comm, Nat.add_sub. rewrite Nat_sub_sub_distr; auto with Arith; rewrite Nat.add_succ_r. rewrite Nat.sub_add; [ idtac | apply Nat.lt_le_incl; auto ]. rewrite Nat.sub_succ_l; [ simpl | apply Nat.lt_le_incl; auto ]. rewrite List.fold_right_app; simpl. rewrite Nat.eqb_refl; simpl. rewrite fold_nothing. apply Hi. rewrite fold_right_eqb_or. simpl in Hlast. destruct pts as [| (l, al)]. injection Hlast; clear Hlast; intros HH H; subst αh. apply Nat2Z.inj in H; subst h. exfalso; apply H₁; reflexivity. eapply IHpts with (αj := αh); try eassumption. intros; apply Hnat with (αi := αi); right; assumption. intros i αi Hpti. apply Sorted_inv_1 in Hsort. simpl in Hpti. destruct Hpti as [H| H]. injection H; clear H; intros; subst l al. apply Sorted_inv in Hsort. destruct Hsort as (_, Hrel). apply HdRel_inv in Hrel. progress unfold fst_lt in Hrel; simpl in Hrel. apply Qnat_lt; assumption. apply Sorted_minus_2nd in Hsort. revert Hsort H; clear; intros. revert h i αi Hsort H. induction pts as [| (l, al)]; [ contradiction | intros ]. destruct H as [H| H]. injection H; clear H; intros; subst l al. apply Sorted_inv in Hsort. destruct Hsort as (_, Hrel). apply HdRel_inv in Hrel. progress unfold fst_lt in Hrel; simpl in Hrel. apply Qnat_lt; assumption. eapply IHpts; [ idtac | eassumption ]. eapply Sorted_minus_2nd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Qlt_trans; eassumption. intros; eapply Qlt_trans; eassumption. eapply Sorted_inv_1; eassumption. apply Nat.lt_succ_r; reflexivity. intros i Hji Hij. remember Hji as H; clear HeqH. rewrite Nat.add_sub_assoc in Hij; auto with Arith; clear H. rewrite Nat.add_sub_swap, Nat.sub_diag in Hij; auto with Arith. remember (Nat.eqb i h) as b eqn:Hb . symmetry in Hb. destruct b. apply Nat.eqb_eq in Hb. rewrite Hb in Hij. exfalso; revert Hij; apply Nat.lt_irrefl. simpl. apply Sorted_inv_1 in Hsort. revert Hnat Hsort Hij; clear; intros. revert h i Hnat Hsort Hij. induction pts as [| (l, al)]; intros; [ reflexivity | simpl ]. assert ((l, al) ∈ [(Qnat h, αh); (l, al) … pts]) as H. right; left; reflexivity. apply Hnat in H. destruct H as (m, Hm); subst l; rename m into l. rewrite nat_num_Qnat. remember (Nat.eqb i l) as b eqn:Hb . symmetry in Hb. destruct b; simpl. apply Nat.eqb_eq in Hb; subst l. apply Sorted_inv in Hsort. destruct Hsort as (_, Hrel). apply HdRel_inv in Hrel. progress unfold fst_lt in Hrel; simpl in Hrel. apply Qnat_lt in Hrel. apply Nat.nle_gt in Hrel. exfalso; apply Hrel, Nat.lt_le_incl; assumption. eapply IHpts; try eassumption. intros iq αi Hpti. apply Hnat with (αi := αi). simpl in Hpti. destruct Hpti as [H| H]. injection H; intros; subst. left; reflexivity. right; right; assumption. eapply Sorted_minus_2nd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Qlt_trans; eassumption. Qed.
imports: Utf8 QArith NPeano Sorted ConvexHullMisc ConvexHull PolyConvexHull Field2 Misc Newton NbarM QbarM SplitList Fsummation Fpolynomial Power_series Puiseux_series Ps_add Ps_mul Ps_div Ps_add_compat PSpolynomial Puiseux_base CharactPolyn AlgCloCharPol