proposition: Lemma card_setdiff d k (la : 'P_d) (mu : 'P_(d + k)) : size mu <= n -> size la <= n -> vb_strip la mu -> #|setdiff la mu| = k.
proof: Proof. Proof using . move=> Hszmu Hszla /(vb_stripP (intpartnP _) (intpartnP _)) Hstrip. 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. apply esym; rewrite /setdiff -sum1dep_card -[LHS](addKn d k). rewrite -{2}(sumn_intpartn la) -{1}(sumn_intpartn mu). rewrite (sumn_nth_le Hszmu) (sumn_nth_le Hszla). transitivity (\sum_(0 <= i < n) (nth 0 mu i - nth 0 la i)). rewrite /index_iota subn0. elim: n {Hszmu Hszla} => [//= | j IHj]; first by rewrite !big_nil. rewrite -addn1 iotaD /= add0n !big_cat !big_cons !big_nil /= !addn0. rewrite subnDA subnAC -addnBA // addnC [RHS]addnC -{}IHj. by rewrite addnBA // leq_sum. rewrite !big_mkord [LHS](bigID (fun i : 'I_n => nth 0 la i < nth 0 mu i)) /=. rewrite [X in (_ + X = _)]big1 ?addn0; first last. by move=> i; rewrite -leqNgt -subn_eq0 => /eqP ->. apply eq_bigr => i H. suff -> : nth 0 mu i = (nth 0 la i).+1 by rewrite subSn // subnn. by apply anti_leq; rewrite Hstrip1 H. 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