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