proposition: Lemma mem_take_enumI n (i : 'I_n) k : i \in take k (enum 'I_n) = (i < k).
proof: Proof. case: i => i Hi /=. rewrite -(mem_map val_inj) map_take val_enum_ord /= take_iota mem_iota /= add0n. rewrite /minn; case: (ltnP k n) => //= H. by rewrite Hi (leq_trans Hi H). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)