proposition: Theorem points_of_polyn_sorted : ∀ deg (cl : list (puiseux_series α)) pts, pts = points_of_ps_lap_gen deg cl → Sorted fst_lt pts.
proof: Proof. intros deg cl pts Hpts. destruct cl as [| c₁]; [ subst pts; constructor | idtac ]. revert deg c₁ pts Hpts. induction cl as [| c]; intros. unfold points_of_ps_lap_gen in Hpts; simpl in Hpts. destruct (order c₁); subst pts; constructor; constructor. unfold points_of_ps_lap_gen in Hpts. remember [c … cl] as ccl; simpl in Hpts; subst ccl. destruct (order c₁) as [q | ]; [ idtac | eapply IHcl; eassumption ]. remember (points_of_ps_lap_gen (S deg) [c … cl]) as pts₁. subst pts; rename pts₁ into pts; rename Heqpts₁ into Hpts. clear IHcl. clear c₁. revert deg c q pts Hpts. induction cl as [| c₂]; intros. simpl. unfold points_of_ps_lap_gen in Hpts; simpl in Hpts. destruct (order c). constructor; constructor; [ constructor | constructor | idtac ]. apply Qnat_lt, lt_n_Sn. constructor; constructor. unfold points_of_ps_lap_gen in Hpts. remember [c₂ … cl] as ccl; simpl in Hpts; simpl; subst ccl. destruct (order c) as [v₂| ]. subst pts. apply Sorted_LocallySorted_iff. constructor; [ idtac | apply Qnat_lt, lt_n_Sn ]. apply Sorted_LocallySorted_iff. eapply IHcl; reflexivity. eapply IHcl with (q := q) in Hpts. apply Sorted_minus_2nd with (x₂ := (Qnat (S deg), q)). unfold fst_lt. intros x y z; apply Qlt_trans. constructor; [ assumption | constructor; apply Qnat_lt, lt_n_Sn ]. Qed.
imports: Utf8 QArith Sorting ConvexHull ConvexHullMisc Misc NbarM QbarM Newton Field2 Fpolynomial Power_series Puiseux_series Ps_add Ps_add_compat Ps_mul Ps_div