proposition: Theorem in_pts_in_ppl : ∀ pow cl ppl pts h hv hps def, ppl = qpower_list pow cl → pts = filter_finite_ord ppl → (h, hv) ∈ pts → hps = List.nth (Z.to_nat (Qnum h) - pow) cl def → (h, hps) ∈ ppl ∧ order hps = qfin hv.
proof: Proof. intros pow cl ppl pts h hv hps def Hppl Hpts Hhhv Hhps. subst ppl pts. destruct cl as [| c₁]; intros; [ contradiction | idtac ]. revert pow c₁ h hv hps Hhps Hhhv. induction cl as [| c]; intros. simpl in Hhhv. remember (order c₁) as v. symmetry in Heqv. destruct v as [v| ]; [ idtac | contradiction ]. destruct Hhhv as [Hhhv| ]; [ idtac | contradiction ]. injection Hhhv; clear Hhhv; intros; subst v h. remember (Qnum (Qnat pow)) as x; simpl in Heqx; subst x. rewrite Nat2Z.id, minus_diag in Hhps. simpl in Hhps; subst hps. split; [ left; reflexivity | assumption ]. remember [c … cl] as ccl; simpl in Hhhv; subst ccl. remember (order c₁) as v. symmetry in Heqv. destruct v as [v| ]. destruct Hhhv as [Hhhv| Hhhv]. injection Hhhv; clear Hhhv; intros; subst v h. remember (Qnum (Qnat pow)) as x; simpl in Heqx; subst x. rewrite Nat2Z.id, minus_diag in Hhps. simpl in Hhps; subst hps. split; [ left; reflexivity | assumption ]. destruct (le_dec (S pow) (Z.to_nat (Qnum h))) as [Hle| Hgt]. eapply IHcl in Hhhv. rewrite <- Nat.sub_succ in Hhps. rewrite <- minus_Sn_m in Hhps; [ idtac | assumption ]. simpl in Hhps. destruct Hhhv as (Hhhv, Hhv). split; [ right; eassumption | assumption ]. rewrite <- Nat.sub_succ in Hhps. rewrite <- minus_Sn_m in Hhps; [ idtac | assumption ]. simpl in Hhps; eassumption. apply first_power_le in Hhhv; contradiction. destruct (le_dec (S pow) (Z.to_nat (Qnum h))) as [Hle| Hgt]. eapply IHcl in Hhhv. rewrite <- Nat.sub_succ in Hhps. rewrite <- minus_Sn_m in Hhps; [ idtac | assumption ]. simpl in Hhps. destruct Hhhv as (Hhhv, Hhv). split; [ right; eassumption | assumption ]. rewrite <- Nat.sub_succ in Hhps. rewrite <- minus_Sn_m in Hhps; [ idtac | assumption ]. simpl in Hhps; eassumption. apply first_power_le in Hhhv; contradiction. 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