proposition: Lemma mem_drop_enumI n (i : 'I_n) k : i \in drop k (enum 'I_n) = (i >= k).
proof: Proof. case (leqP k n) => Hkn. - case: i => i Hi /=. rewrite -(mem_map val_inj) map_drop val_enum_ord /= drop_iota mem_iota /= add0n. by rewrite (subnKC Hkn) Hi andbT. - rewrite drop_oversize; last by rewrite size_enum_ord; apply: ltnW. have:= ltn_trans (ltn_ord i) Hkn. by rewrite in_nil ltnNge => /negbTE => ->. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)