proposition: Lemma filter_le_to_word (d : unit) (T : inhOrderType d) n (t : seq (seq T)) : filter (<=%O n) (to_word t) = to_word (filter_le_tab n t).
proof: Proof. Proof using . elim: t => [// | t0 t IHt] /=. rewrite to_word_cons filter_cat /=. case: (filter (<=%O n) t0 =P [::]) => [->|_] /=. - by rewrite cats0 IHt to_word_cons cats0. - by rewrite to_word_cons IHt. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(mpoly) tools ordcast combclass partition skewpart Yamanouchi ordtype std tableau stdtab Schensted congr plactic Greene_inv stdplact Yam_plact skewtab shuffle Schur_mpoly freeSchur