proposition: Lemma famY_bij (mon : 'X_{1.. m}) : mdeg mon = d -> {on [pred i in family (fun i0 (j : 'X_{1.. n < d.+1}) => mdeg j == tnth mon i0)], bijective famY}.
proof: Proof. move=> Hdeg; exists famYinv. - move=> mz; rewrite inE => /familyP Hff. apply val_inj => /=; rewrite /famYinv_fun. rewrite (([multinom _ | i < m * n] =P val mz) _) /= ?bmdeg //. apply/eqP/mnmP => c; rewrite mnmE /famY ffunE /=. by rewrite tnth_mktuple mnmE //= -[in RHS](vecmx_indexK c). - move=> ff; rewrite inE => /familyP H /=. apply/ffunP => /= i; rewrite ffunE; apply val_inj => /=. rewrite /famYinv_fun [mdeg _](_ : _ = d) ?ltnSn; first last. rewrite -[RHS]Hdeg !mdegE big_mxvec_index => /=; apply eq_bigr => i' _. have {H} := H i'; rewrite unfold_in mnm_tnth => /eqP <-. rewrite mdegE; apply eq_bigr => j _. by rewrite mnmE mxvec_indexK /=. by rewrite tnth_mktuple; apply mnmP => j; rewrite !mnmE mxvec_indexK /=. 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