proposition: Lemma picks_remove k a l : picks k (filter (no (Nat.eqb a)) l) = filter (no (appears a)) (picks k l).
proof: Proof. induction k. reflexivity. simpl. rewrite IHk. clear IHk. generalize (picks k l); intros ll. rewrite cartesian_product_filters. induction (cartesian_product l ll) as [| a0 l0 IHl0]. simpl. reflexivity. simpl. rewrite <-IHl0. unfold no. simpl. destruct (a =? fst a0). reflexivity. simpl. destruct (appears a (snd a0)); reflexivity. Qed.
imports: Arith ZArith List Lia