proposition: Lemma count_sumtrue_cons_false p l : filter (sumtrue p) (map (cons false) l) = map (cons false) (filter (sumtrue p) l).
proof: Proof. induction l; auto. simpl. change (sumtrue p (false :: a)) with (sumtrue p a). destruct (sumtrue p a); auto. simpl. congruence. Qed.
imports: Arith ZArith String List Psatz Factorial