proposition: Theorem in_pts_in_psl : ∀ pow pts psl h hv hps def, pts = filter_finite_ord (qpower_list pow psl) → (h, hv) ∈ pts → hps = List.nth (Z.to_nat (Qnum h) - pow) psl def → hps ∈ psl ∧ order hps = qfin hv.
proof: Proof. intros pow pts psl h hv hps def Hpts Hhv Hhps. remember (power_list pow psl) as ppl. assert (pow ≤ Z.to_nat (Qnum h)) as H. subst pts ppl. eapply first_power_le; eassumption. eapply in_pts_in_ppl in Hhv; try eassumption; [ idtac | reflexivity ]. destruct Hhv as (Hhps₁, Hv). split; [ idtac | assumption ]. subst ppl. destruct psl as [| ps₁]; [ contradiction | idtac ]. revert pow pts ps₁ h hv hps Hhps Hv Hhps₁ Hpts H. induction psl as [| ps]; intros. destruct Hhps₁ as [Hhps₁| ]; [ idtac | contradiction ]. injection Hhps₁; clear Hhps₁; intros; subst h hps. now left. destruct Hhps₁ as [Hhps₁| Hhps₁]. injection Hhps₁; clear Hhps₁; intros; subst h hps. now left. destruct (eq_nat_dec (Z.to_nat (Qnum h)) pow) as [Heq| Hne]. rewrite Heq, minus_diag in Hhps. subst hps; left; reflexivity. right. eapply IHpsl; try eassumption; try reflexivity. rewrite <- Nat.sub_succ in Hhps. rewrite <- minus_Sn_m in Hhps; [ assumption | idtac ]. apply not_eq_sym in Hne. apply Nat_le_neq_lt; assumption. apply not_eq_sym in Hne. apply Nat_le_neq_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