proposition: Theorem list_length_shrink_le : ∀ k (l : list α), length (list_shrink k l) ≤ length l.
proof: Proof. intros k l. unfold list_shrink. assert (∀ cnt k₁, length (list_shrink_aux cnt k₁ l) ≤ length l) as H. intros cnt k₁. revert cnt. induction l as [| x]; intros; [ reflexivity | simpl ]. destruct cnt; simpl. apply le_n_S, IHl. etransitivity; [ apply IHl | idtac ]. apply Nat.le_succ_r; left; reflexivity. apply H. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn