proposition: Lemma pickbools_wins_minus p q : q <= p -> (p - q) * length (filter (sumtrue p) (pickbools (p + q))) = (p - q) * length (filter winb (filter (sumtrue p) (pickbools (p + q)))).
proof: Proof. intros L. assert (D : q = p \/ q < p) by lia. destruct D as [D | D]. - replace (p - q) with 0 by lia. lia. - clear L. f_equal. f_equal. rewrite counting_wins; auto. Qed.
imports: Arith ZArith String List Psatz Factorial