proposition: Theorem length_shrink_skipn_lt : ∀ k (l : list α) m, (length l < S k)%nat → length (list_shrink_aux 0 m (List.skipn k l)) = 0%nat.
proof: Proof. intros k l m Hk. revert k m Hk. induction l as [| x]; intros; [ destruct k; reflexivity | simpl ]. simpl in Hk. apply Nat.succ_lt_mono in Hk. destruct k. exfalso; revert Hk; apply Nat.nlt_0_r. simpl; apply IHl; 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