proposition: Lemma pred_count_eq_none_inv : forall (A : Set)(P : A -> Prop)(ls : list A) c, pred_count P ls c -> (forall a, In a ls -> ~P a) -> c = O.
proof: Proof. induction 1; intuition; simpl in *. exfalso. eapply H1. eauto. trivial. eapply IHpred_count. intuition. eapply H1; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation