proposition: Theorem Sorted_fst_2nd_lt_last : ∀ j αj k αk t₁ t₂ t₃ tl, Sorted (λ pt₁ pt₂, Qnum (fst pt₁) < Qnum (fst pt₂)) [t₁; t₂; t₃ … tl] → (Qnat j, αj) = t₁ → (Qnat (S k), αk) = List.last [t₃ … tl] (0, 0)%Q → (nat_num (fst t₂) < S k)%nat.
proof: Proof. intros j αj k αk t₁ t₂ t₃ tl Hsort Hj Hk. revert k αk t₃ Hsort Hk. induction tl as [| t₄]; intros. simpl in Hk. apply Sorted_inv in Hsort. destruct Hsort as (Hsort, Hrel). apply Sorted_inv in Hsort. destruct Hsort as (Hsort, Hrel₁). apply HdRel_inv in Hrel₁. rewrite <- Hk in Hrel₁; remember (S k) as x; simpl in Hrel₁; subst x. apply Z2Nat.inj_lt in Hrel₁. rewrite Nat2Z.id in Hrel₁. assumption. apply Z.lt_le_incl. apply HdRel_inv in Hrel. subst t₁. simpl in Hrel. eapply Z.le_lt_trans; [ apply Nat2Z.is_nonneg | eassumption ]. apply Nat2Z.is_nonneg. remember [t₄ … tl] as x; simpl in Hk; subst x. eapply IHtl; try eassumption. eapply Sorted_minus_3rd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Z.lt_trans; 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