proposition: Lemma mem_index_enum T i : i \in index_enum T.
proof: Proof. by rewrite [index_enum T]unlock -enumT mem_enum. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)