proposition: Theorem bertrand_ballot p q : let l := filter (fun votes => count_votes votes "A" =? p)%nat (picks (p + q) ["A"; "B"]) in p >= q -> (p + q) * List.length (filter (throughout (wins "A" "B")) l) = (p - q) * List.length (filter (wins "A" "B") l).
proof: Proof. intros l L; subst l. pose (f := fun b : bool => if b then "A" else "B"). replace (picks (p + q) ["A"; "B"]) with (map (map f) (pickbools (p + q))); swap 1 2. { generalize (p + q). clear p q L. induction n. reflexivity. simpl. do 2 rewrite map_app. f_equal. 2:rewrite app_nil_r. all: rewrite <- IHn. all: generalize (pickbools n); intros l; induction l; simpl; congruence. } repeat rewrite map_filter. repeat rewrite map_length. assert (A : forall b l, count_votes (map f l) (f b) = countb b l). { clear. intros b l; induction l; auto. simpl. destruct a, b; simpl; auto. } assert (E : forall l, wins "A" "B" (map f l) = winb l). { clear -A. unfold wins, winb. intros l. f_equal. apply (A false). apply (A true). } etransitivity; [ | etransitivity ]; [ | apply (bertrand_ballot_bool p q); auto | ]; f_equal. - f_equal. repeat rewrite filter_filter. apply filter_ext. intros l. f_equal. + unfold sumtrue. f_equal. induction l as [ | b l IHl]; auto. simpl. destruct b; auto. simpl. auto. + unfold throughout, proper_suffixes. induction l as [ | b l IHl]; auto. simpl. f_equal; auto. rewrite <-E. auto. - f_equal. repeat rewrite filter_filter. apply filter_ext. intros l; f_equal. 2:now auto. unfold sumtrue. f_equal. rewrite <-A. auto. Qed.
imports: Arith ZArith String List Psatz Factorial