proposition: Theorem ord_is_ord_of_pt : ∀ pl h, Sorted fst_lt pl → (∀ pt, pt ∈ pl → ∃ (h : nat) (αh : Q), pt = (Qnat h, αh)) → h ∈ List.map (λ x, nat_num (fst x)) pl → (Qnat h, ord_of_pt h pl) ∈ pl.
proof: Proof. intros pl h Hsort Hnat Hin. induction pl as [| (l, al)]; [ contradiction | simpl ]. destruct (Qeq_dec (Qnat h) l) as [H| H]. simpl in Hin. destruct Hin as [Hin| Hin]. left; subst h. assert ((l, al) ∈ [(l, al) … pl]) as Hpt by (left; reflexivity). apply Hnat in Hpt. destruct Hpt as (h, (ah, Hpt)). injection Hpt; clear Hpt; intros; subst l al. rewrite nat_num_Qnat; simpl. reflexivity. exfalso. clear - Hnat Hsort Hin H. revert al h Hnat Hsort Hin H. induction pl as [| (m, am)]; intros; [ contradiction | simpl ]. simpl in Hin. destruct Hin as [Hin| Hin]. subst h. apply Sorted_inv_2 in Hsort. destruct Hsort as (Hrel, Hsort). progress unfold fst_lt in Hrel; simpl in Hrel. rewrite <- H in Hrel. progress unfold Qnat, nat_num in Hrel. assert ((m, am) ∈ [(l, al); (m, am) … pl]) as Hpt by (right; left; reflexivity). apply Hnat in Hpt. destruct Hpt as (p, (ap, Hp)). injection Hp; clear Hp; intros; subst m am. rewrite Z2Nat.id in Hrel; simpl in Hrel. simpl in Hrel. revert Hrel; apply Z.lt_irrefl. apply Nat2Z.is_nonneg. apply Sorted_minus_2nd in Hsort. eapply IHpl; try eassumption. intros pt Hpt. apply Hnat. destruct Hpt as [Hpt| Hpt]. rewrite Hpt; left; reflexivity. right; right; assumption. intros x y z H₁ H₂; eapply Qlt_trans; eassumption. right. apply IHpl. eapply Sorted_inv_1; eassumption. intros pt Hpt. apply Hnat. right; assumption. destruct Hin as [Hin| Hin]; [ idtac | assumption ]. simpl in Hin. exfalso; apply H; clear H. subst h. assert ((l, al) ∈ [(l, al) … pl]) as Hpt by (left; reflexivity). apply Hnat in Hpt. destruct Hpt as (p, (ap, Hp)). injection Hp; clear Hp; intros; subst l al. rewrite nat_num_Qnat; reflexivity. 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