proposition: Fact famY_subproof (mz : 'X_{1.. (m * n) < d.+1}) i : (mdeg (tnth (monsY (val mz)) i) < d.+1)%N.
proof: Proof. apply: (leq_ltn_trans _ (bmdeg mz)). rewrite /mdeg /monsY tnth_mktuple !big_tuple big_mxvec_index /=. under eq_bigr do rewrite tnth_mktuple mnm_tnth. by rewrite (bigD1 i) //= leq_addr. 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