proposition: Lemma vecmx_indexK i : mxvec_index (vecmx_index i).1 (vecmx_index i).2 = i.
proof: Proof. rewrite /vecmx_index/mxvec_index/uncurry/=. case H : (enum_val (cast_ord (esym (mxvec_cast m n)) i)) => /= [a b]. by rewrite -H enum_valK cast_ordKV. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssrint rat ssralg ssrnum algC matrix vector) mathcomp(mpoly) tools partition ordtype antisym Schur_mpoly Schur_altdef sympoly homogsym permcent