proposition: Lemma filtergtn_LRsupport Q : Q \in LRsupport (hyper_stdtabn P1) (hyper_stdtabn P2) -> filter_gt_tab d1 Q = hyper_stdtabn P1.
proof: Proof. Proof using . rewrite inE. move/(pred_LRtriple_fast_filter_gt (stdtabnP (hyper_stdtabn P1)) (stdtabnP Q)) => ->. by rewrite size_tab_stdtabn. 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