proposition: Lemma nohasincr_setdiff d k (la : 'P_d) (mu : 'P_(d + k)) : size mu <= n -> size la <= n -> vb_strip la mu -> ~~ hasincr la (setdiff la mu).
proof: Proof. Proof using . move=> Hszmu Hszla Hstrip. apply/hasPn => i; rewrite mem_iota add0n => /andP[_ Hi]. rewrite /mnm_add [val _]/= !nth_add_setdiff //. rewrite eq_sym ltn_eqF // ltnS. by have [_]:= (is_partP _ (intpartnP mu)); apply. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(mpoly) tools combclass ordtype sorted partition tableau skewpart skewtab antisym Schur_mpoly freeSchur therule std stdtab unitriginv presentSn