proposition: Lemma counting_wins p q : q < p -> filter winb (filter (sumtrue p) (pickbools (p + q))) = filter (sumtrue p) (pickbools (p + q)).
proof: Proof. intros. rewrite pickbools_length. repeat rewrite filter_filter. apply filter_ext. intros x. unfold winb, sumtrue. destruct (length x =? p + q) eqn:E. 2:reflexivity. simpl. destruct (countb true x =? p) eqn:E2. 2:reflexivity. simpl. rewrite countb_false. rewrite Nat.ltb_lt. rewrite Nat.eqb_eq in *. lia. Qed.
imports: Arith ZArith String List Psatz Factorial