proposition: Lemma vb_strip_lexi (d1 k : nat) (la : 'P_(d1 + k)) (mu : seq nat) : vb_strip mu la -> sumn mu = d1 -> is_part mu -> (val la <= incr_first_n mu k :> seqlexi nat)%O.
proof: Proof. Proof using . rewrite /=. elim: mu d1 k la => /= [| m0 mu IHmu] d1 k la Hstr. have {}Hstr := vb_stripP (is_true_true : is_part [::]) (intpartnP _) Hstr. move=> Hd1 _; subst d1. suff /= -> : val la = nseq k 1%N by []. case: la Hstr => la /=; rewrite add0n => /andP[/eqP]. elim: la k => [//= | l0 la IHla] /= k Hk; first by rewrite -Hk. rewrite -/(is_part (l0 :: la)) => Hpart Hstr. have Hl0 : l0 = 1. have := Hstr 0 => /=. have /= := part_head_non0 Hpart. by case l0 => [| [| l0']]. subst l0; rewrite -Hk add1n /= {1}(IHla (sumn la)) //. - exact: (is_part_consK Hpart). - move=> i; have /= := Hstr i.+1. by rewrite !nth_nil. case: la Hstr => la Hla /= Hstr. case: k Hla => [| k] Hla Hd1; subst d1; rewrite -/(is_part (m0 :: mu)) /= => /andP[_ Hp]. have Hincl := vb_strip_included Hstr. move: Hla; rewrite addn0 /= -/(sumn (m0 :: mu)) => /andP[/eqP/esym Heq Hla]. by rewrite (included_sumnE Hla Hincl Heq). case: la Hstr Hla => [//= |s0 la] /= /andP[/andP[ms0 sm0] Hstrip]. move=> /andP[/eqP Heq /andP[_ Hs]]. rewrite leEseqlexi leEnat sm0 /=. case: (leqP s0 m0) => //= Hm0. have Hs0 : s0 = m0.+1 by apply anti_leq; rewrite Hm0 sm0. subst s0 => /= {Hm0}. move: Heq; rewrite addSn addnS => /eqP; rewrite eqSS -addnA => /eqP /addnI Heq. have Hla : is_part_of_n (sumn mu + k)%N la. by rewrite /= Heq eq_refl Hs. exact: (IHmu _ _ (IntPartN Hla)). 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