proposition: Lemma big_mxvec_index P F : \big[op/idx]_(i : 'I_(m * n) | P i) F i = \big[op/idx]_(i < m) \big[op/idx]_(j < n | P (mxvec_index i j)) F (mxvec_index i j).
proof: Proof. rewrite pair_big_dep. rewrite (reindex (uncurry mxvec_index)); first last. by apply: (subon_bij _ (curry_mxvec_bij m n)). by apply eq_big => [] [i j]. 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