proposition: Lemma bertrand_ballot_bool_eq p q : p <> 0 -> p = q -> let l := filter (fun votes => countb true votes =? p) (pickbools (p + q)) in (p + q) * length (filter (throughout winb) l) = (p - q) * length (filter winb l).
proof: Proof. intros L <-. replace (p - p) with 0 by lia. simpl. match goal with |- ?a * ?b = 0 => cut (b = 0) end. intros ->; auto. rewrite pickbools_length. transitivity (length (filter (fun _ => false) (pickbools (p + p)))). - f_equal. rewrite pickbools_length. repeat rewrite filter_filter. apply filter_ext. intros x. destruct (length x =? p + p) eqn:Hlen; auto. simpl. destruct (countb true x =? p) eqn:Hp; auto. simpl. rewrite Nat.eqb_eq in *. destruct x. simpl in *. lia. unfold throughout. simpl. unfold winb. rewrite countb_false. rewrite Hlen, Hp. replace (p + p - p) with p by lia. rewrite Nat.ltb_irrefl. reflexivity. - generalize (pickbools (p + p)). generalize (list bool). clear. intros P l. induction l; auto. Qed.
imports: Arith ZArith String List Psatz Factorial