proposition: Theorem Sorted_fst_lt_nat_num_fst : ∀ l, (∀ a, a ∈ l → fst a = Qnat (Z.to_nat (Qnum (fst a)))) → Sorted fst_lt l → Sorted (λ x y, (nat_num (fst x) < nat_num (fst y))%nat) l.
proof: Proof. intros l Hnat Hsort. apply Sorted_LocallySorted_iff in Hsort. apply Sorted_LocallySorted_iff. induction l as [| a]; [ constructor | idtac ]. destruct l as [| b]; constructor. apply IHl. intros c Hc. apply Hnat; right; assumption. inversion Hsort; assumption. inversion Hsort; subst. rewrite Hnat; [ idtac | left; reflexivity ]. apply Nat.nle_gt. rewrite Hnat; [ idtac | right; left; reflexivity ]. apply Nat.nle_gt. do 2 rewrite nat_num_Qnat. unfold fst_lt in H3. rewrite Hnat in H3; [ idtac | left; reflexivity ]. apply Qlt_not_le in H3. rewrite Hnat in H3; [ idtac | right; left; reflexivity ]. apply Qnot_le_lt in H3. apply Qnat_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