proposition: Lemma drop_enumI n k : drop k (enum 'I_n) = filter ((leq k) \o val) (enum 'I_n).
proof: Proof. apply: (inj_map val_inj); rewrite map_drop map_filter_comp val_enum_ord. rewrite drop_iota add0n. case: (leqP n k) => Hk. - have:= Hk; rewrite -subn_eq0 => /eqP -> /=. rewrite (eq_in_filter (a2 := pred0)); first by rewrite filter_pred0. move=> i; rewrite mem_iota add0n => /andP[_ Hi]. have:= leq_trans Hi Hk. by rewrite ltnNge => /negbTE => ->. - move Hdiff : (n - k) => d; move: Hdiff => /eqP. rewrite -(eqn_add2r k) subnK; last exact: ltnW. move/eqP -> => {n Hk}. rewrite addnC iotaD filter_cat map_id add0n. rewrite (eq_in_filter (a2 := pred0)); first last. move=> i; rewrite mem_iota add0n => /andP[_ Hi]. by move: Hi; rewrite ltnNge => /negbTE => ->. rewrite filter_pred0 cat0s. rewrite (eq_in_filter (a2 := predT)); first by rewrite filter_predT. by move=> i; rewrite mem_iota => /andP[->]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)