proposition: Lemma included_shape_filter_gt_tab (d : unit) (T : inhOrderType d) (n : T) t : is_tableau t -> included (shape (filter_gt_tab n t)) (shape t).
proof: Proof. Proof using . elim: t => [// | r0 t /= IHt] /= /and4P[Hnnil Hrow Hdom Htab]. case: ([seq x <- r0 | (x < n)%O] =P [::]) => [Hr0 | _] /=. rewrite (filter_le_first_row0 Htab Hdom Hr0). by rewrite (_ : filter _ _ = [::]); last by elim: (size t). by rewrite size_filter count_size (IHt Htab). 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