proposition: Lemma pred_count_left_total : forall (A : Type)(P : A -> Prop)(ls : list A), (forall a, P a \/ ~P a) -> exists c, pred_count P ls c.
proof: Proof. induction ls; intuition. exists O. econstructor. destruct H0. destruct (H a). exists (S x). econstructor; eauto. exists x. econstructor; eauto. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation