proposition: Lemma pred_count_eq_none : forall (A : Type)(P : A -> Prop)(ls : list A), (forall a, In a ls -> ~P a) -> pred_count P ls 0.
proof: Proof. induction ls; intuition; simpl in *. econstructor. econstructor; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation