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