proposition: Theorem Sorted_Qnat_Sorted_Qnum : ∀ pts, Sorted fst_lt pts → List.Forall (λ pt, Qden (fst pt) = 1%positive) pts → Sorted (λ pt₁ pt₂, Qnum (fst pt₁) < Qnum (fst pt₂)) pts.
proof: Proof. intros pts Hsort Hden1. apply Sorted_LocallySorted_iff in Hsort. apply Sorted_LocallySorted_iff. induction pts as [| pt]; [ constructor | idtac ]. destruct pts as [| pt₂]; constructor. apply IHpts. inversion Hsort; assumption. eapply list_Forall_inv; eassumption. inversion Hsort; subst. apply list_Forall_inv in Hden1. destruct Hden1 as (Hden1, H). apply list_Forall_inv in H. destruct H as (Hden₂, _). unfold fst_lt in H3. unfold Qlt in H3. rewrite Hden1, Hden₂ in H3. do 2 rewrite Z.mul_1_r in H3; 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