proposition: Lemma pred_count_app : forall (A : Type)(P : A -> Prop)(ls1 ls2 : list A) n1 n2, pred_count P ls1 n1 -> pred_count P ls2 n2 -> pred_count P (ls1 ++ ls2) (n1 + n2).
proof: Proof. induction ls1; intuition; simpl in *. inversion H; subst; clear H. simpl. trivial. inversion H; clear H; subst. simpl. econstructor; eauto. econstructor; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation