proposition: Lemma pred_count_first_skip : forall (A : Type)(P : A -> Prop)(ls : list A)(c : nat), pred_count P ls c -> forall n, exists c1 c2, pred_count P (firstn n ls) c1 /\ pred_count P (skipn n ls) c2 /\ (c1 + c2 = c)%nat.
proof: Proof. induction 1; intuition; simpl in *. exists O. exists O. intuition; destruct n; simpl; econstructor. destruct n0; simpl. destruct (IHpred_count O). destruct H1. intuition. subst. exists x. exists (S x0). intuition. econstructor; trivial. destruct (IHpred_count n0). destruct H1. destruct H1. intuition. subst. exists (S x). exists x0. intuition. econstructor; trivial. destruct n0; simpl. destruct (IHpred_count O). destruct H1. intuition. subst. exists x. exists x0. intuition. econstructor; trivial. destruct (IHpred_count n0). destruct H1. destruct H1. intuition. subst. exists x. exists x0. intuition. econstructor; trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation