proposition: Lemma take_enumI n k : take k (enum 'I_n) = filter ((gtn k) \o val) (enum 'I_n).
proof: Proof. apply: (inj_map val_inj); rewrite map_take map_filter_comp val_enum_ord. rewrite take_iota /minn. case: (ltnP k n) => Hk. - elim: k n Hk => [//= | k IHk] n Hk /=. + by rewrite (eq_filter (a2 := pred0)) // filter_pred0. + case: n Hk => [//= | n] Hk /=. rewrite -[1]addn0 !iotaDl (IHk _ Hk). by rewrite filter_map /= -!map_comp. - rewrite (eq_in_filter (a2 := predT)); first by rewrite filter_predT map_id. move=> i /=; rewrite mem_iota add0n => /andP[_ H2]. by rewrite (leq_trans H2 Hk). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)