proposition: Theorem list_length_shrink : ∀ cnt k (l : list α), (S cnt < length l)%nat → List.length (list_shrink_aux cnt k l) = S ((List.length l - S cnt) / S k).
proof: Proof. intros cnt k l Hcl. revert cnt k Hcl. induction l; intros. exfalso; revert Hcl; apply Nat.nlt_0_r. remember (S k) as k'; simpl; subst k'. remember (S k) as k'; destruct cnt; simpl; subst k'. rewrite Nat.sub_0_r. apply Nat.succ_inj_wd. destruct (lt_eq_lt_dec (S k) (length l)) as [[H₁| H₁]| H₁]. rewrite IHl; [ idtac | assumption ]. simpl in Hcl. assert (length l = length l - S k + 1 * S k)%nat as H. rewrite Nat.mul_1_l. rewrite Nat.sub_add; auto with Arith. apply Nat.lt_le_incl; auto with Arith. rewrite H in |- * at 2; clear H. rewrite Nat.div_add; [ idtac | intros H; discriminate H ]. rewrite Nat.add_1_r; reflexivity. rewrite <- H₁. rewrite Nat.div_same; auto with Arith. rewrite list_shrink_skipn. apply length_shrink_skipn_eq; symmetry; assumption. rewrite Nat.div_small; [ idtac | assumption ]. rewrite list_shrink_skipn. apply length_shrink_skipn_lt; assumption. simpl in Hcl. apply Nat.succ_lt_mono in Hcl. 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