proposition: Lemma Zlength_picks {A} n (l : list A) : Zlength (picks n l) = Z.pow (Zlength l) (Z.of_nat n).
proof: Proof. rewrite Zlength_correct. induction n. reflexivity. simpl (length _). rewrite map_length, length_cartesian_product. change (S n) with (1 + n). rewrite Nat2Z.inj_add, Z.pow_add_r, Z.pow_1_r. rewrite <-IHn. rewrite Nat2Z.inj_mul, Zlength_correct. reflexivity. all: zify; lia. Qed.
imports: Arith ZArith List Lia