proposition: Lemma mxvec_indexK i j : vecmx_index (mxvec_index i j) = (i, j).
proof: Proof. rewrite /vecmx_index/mxvec_index/uncurry/=. by rewrite cast_ordK enum_rankK. 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