proposition: Theorem list_nth_coeff_last : ∀ f j αj k αk tl, (Qnat j, αj) = List.hd (0, 0)%Q tl → (Qnat k, αk) = List.last tl (0, 0)%Q → (j < k)%nat → Sorted (λ pt₁ pt₂, Qnum (fst pt₁) < Qnum (fst pt₂)) tl → List.Forall (λ pt, Qden (fst pt) = xH) tl → List.nth (k - j) (make_char_pol R j (List.map (term_of_point f) tl)) 0%K = coeff (term_of_point f (List.last tl (0, 0)%Q)).
proof: Proof. intros f j αj k αk tl Hj Hk Hjk Hsort Hden; simpl. destruct tl as [| t₁]. simpl in Hj, Hk. injection Hj; clear Hj; intros; subst αj. injection Hk; clear Hk; intros; subst αk. rewrite <- Nat2Z.inj_0 in H0. rewrite <- Nat2Z.inj_0 in H1. apply Nat2Z.inj in H0. apply Nat2Z.inj in H1. subst j k. exfalso; revert Hjk; apply Nat.lt_irrefl. simpl in Hj; rewrite <- Hk, <- Hj; simpl. rewrite nat_num_Qnat, Nat.sub_diag, list_pad_0. destruct tl as [| t₂]. simpl in Hk; subst t₁. injection Hk; clear Hk; intros. apply Nat2Z.inj in H0; subst k. exfalso; revert Hjk; apply Nat.lt_irrefl. simpl. remember (k - j)%nat as kj eqn:Hkj . symmetry in Hkj. destruct kj; [ exfalso; fast_omega Hjk Hkj | idtac ]. destruct k; [ discriminate Hkj | idtac ]. rewrite Nat.sub_succ_l in Hkj; [ idtac | fast_omega Hjk ]. apply eq_add_S in Hkj; subst kj. revert j αj k αk t₁ t₂ Hj Hk Hjk Hsort Hden. induction tl as [| t₃]; intros. simpl in Hk; subst t₂; simpl. rewrite nat_num_Qnat. remember (S k) as x; simpl; subst x. rewrite Nat.sub_succ. rewrite list_nth_pad_sub; [ rewrite Nat.sub_diag | idtac ]; reflexivity. simpl. rewrite list_nth_pad_sub. rewrite Nat_sub_sub_distr. rewrite Nat.add_succ_r. rewrite Nat.sub_add; [ idtac | fast_omega Hjk ]. rewrite Nat.sub_succ_l. simpl. destruct t₂ as (h₁, αh₁). eapply IHtl with (αj := αh₁); try eassumption; try reflexivity. eapply Sorted_fst_2nd_lt_last; eassumption. unfold Qnat, nat_num; simpl. rewrite Z2Nat.id. apply Sorted_inv in Hsort. destruct Hsort as (Hsort, Hrel). simpl. apply list_Forall_inv in Hden. destruct Hden as (_, Hden). apply list_Forall_inv in Hden. destruct Hden as (Hden, _). simpl in Hden. rewrite <- Hden. destruct h₁; assumption. rewrite <- Hj in Hsort. apply Sorted_inv in Hsort. destruct Hsort as (_, H). apply HdRel_inv in H. unfold Qnat in H; simpl in H. apply Z.lt_le_incl. eapply Z.le_lt_trans; [ apply Nat2Z.is_nonneg | eassumption ]. unfold Qnat, nat_num; simpl; rewrite Z2Nat.id. constructor; [ reflexivity | idtac ]. apply list_Forall_inv in Hden. destruct Hden as (_, H). apply list_Forall_inv in H. destruct H as (_, H); assumption. rewrite <- Hj in Hsort. apply Sorted_inv in Hsort. destruct Hsort as (_, H). apply HdRel_inv in H. unfold Qnat in H; simpl in H. apply Z.lt_le_incl. eapply Z.le_lt_trans; [ apply Nat2Z.is_nonneg | eassumption ]. apply Nat.lt_succ_r. eapply Sorted_fst_2nd_lt_last; eassumption. subst t₁. apply Sorted_inv in Hsort. destruct Hsort as (_, H). apply HdRel_inv in H; simpl in H. apply Z2Nat.inj_lt in H. rewrite Nat2Z.id in H. assumption. apply Nat2Z.is_nonneg. apply Z.lt_le_incl. eapply Z.le_lt_trans; [ apply Nat2Z.is_nonneg | eassumption ]. remember (nat_num (fst t₂)) as h₁ eqn:Hh₁ . remember (h₁ - S j)%nat as x. rewrite <- Nat.sub_succ; subst x. apply Nat.sub_le_mono_r. apply Nat.le_le_succ_r. apply Nat.lt_succ_r. subst h₁. eapply Sorted_fst_2nd_lt_last; eassumption. 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