proposition: Theorem list_shrink_skipn : ∀ cnt k (l : list α), list_shrink_aux cnt k l = list_shrink_aux 0 k (List.skipn cnt l).
proof: Proof. intros cnt k l. revert cnt. induction l as [| x]; intros; [ idtac | simpl ]. destruct cnt; reflexivity. destruct cnt; [ reflexivity | simpl ]. apply IHl. 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