proposition: Lemma nth_add_setdiff d k (la : 'P_d) (mu : 'P_(d + k)) : size mu <= n -> size la <= n -> vb_strip la mu -> forall i, nth 0 [seq (mpart la) i0 + (mesym1 (setdiff la mu)) i0 | i0 : 'I_n] i = nth 0 mu i.
proof: Proof. Proof using . move=> Hszmu Hszla /(vb_stripP (intpartnP _) (intpartnP _)) Hstrip i. have Hstrip1 j : nth 0 mu j <= (nth 0 la j).+1 by have /andP[] := Hstrip j. have {}Hstrip j : nth 0 la j <= nth 0 mu j by have /andP[] := Hstrip j. case: (ssrnat.ltnP i n) => Hi; first last. rewrite !nth_default //. - exact: leq_trans Hszmu Hi. - by rewrite size_map size_enum_ord. have H0 : 0 < n by apply: (leq_ltn_trans _ Hi). rewrite /mpart Hszla. rewrite !(nth_map (Ordinal H0) 0) ?size_enum_ord // !mnmE. rewrite inE /= (nth_enum_ord (Ordinal H0) Hi). case: ssrnat.ltnP => H /=; rewrite ?addn0 ?addn1. - by apply anti_leq; rewrite H Hstrip1. - by apply anti_leq; rewrite H Hstrip. 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