proposition: Lemma count_sumtrue p n : length (filter (sumtrue p) (pickbools n)) = binomial n p.
proof: Proof. revert p. induction n; intros p. simpl. destruct p; reflexivity. simpl (pickbools _). rewrite filter_app, app_length. destruct p. - replace (binomial (S n) 0) with (0 + binomial (S n) 0) by auto; f_equal. + clear. induction (pickbools n); auto. + rewrite count_sumtrue_cons_false, map_length. rewrite IHn. destruct n; auto. - simpl. f_equal; rewrite <-IHn. all: rewrite map_filter, map_length; reflexivity. Qed.
imports: Arith ZArith String List Psatz Factorial