proposition: Lemma mem_takeP (T : eqType) x0 x k (s : seq T) : reflect (exists2 i, i < minn k (size s) & x = nth x0 s i) (x \in take k s).
proof: Proof. by apply: (iffP (@nthP _ _ _ x0)) => [] [i]; rewrite size_take -/(minn _ _) => isz; do [move <-|move ->]; exists i => //; rewrite nth_take //; exact: leq_trans isz (geq_minl _ _). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)