proposition: Lemma enum_split k : enum I = take (indx k) (enum I) ++ k :: drop (indx k).+1 (enum I).
proof: Proof. rewrite -{2}(@nth_index I k k (enum I)) ?mem_enum //. by rewrite -drop_nth ?index_mem ?mem_enum // cat_take_drop. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap) mathcomp(fintype tuple finfun)