proposition: Lemma first_vote_split p q : filter (sumtrue (1 + p)) (pickbools (1 + p + q)) = map (cons true) (filter (sumtrue p) (pickbools (p + q))) ++ map (cons false) (filter (sumtrue (1 + p)) (pickbools (p + q))).
proof: Proof. simpl (pickbools _). rewrite filter_app. rewrite map_filter. rewrite map_filter. reflexivity. Qed.
imports: Arith ZArith String List Psatz Factorial