proposition: Lemma vb_strip_rem_col0 d (la : 'P_d) : vb_strip (conj_part (behead (conj_part la))) la.
proof: Proof. Proof using . rewrite -{2}(conj_intpartnK la) /=. have Hc : is_part (conj_part la) by apply is_part_conj. apply hb_strip_conj => //; first by apply is_part_behead. elim: {d la} (conj_part la) Hc => [| s0 s IHs] //= /andP[H0 {}/IHs]. case: s H0 => [| s1 s]//= -> ->. by rewrite leqnn. 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