proposition: Lemma mxvec_indexP k : is_mxvec_index k.
proof: Proof. rewrite -[k](cast_ordK (esym mxvec_cast)) esymK. by rewrite -[_ k]enum_valK; case: (enum_val _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)