proposition: Lemma filterleq_LRsupport Q : Q \in LRtab_set P1 P2 P -> (skew_reshape P1 P [seq x <- to_word Q | d1 <= x]) = filter_le_tab d1 Q.
proof: Proof. Proof using . rewrite /LRtab_set inE => /andP[HLR /eqP Hshape]. rewrite /filter_le_tab -Hshape filter_le_to_word /=. have -> : val P1 = shape (filter_gt_tab d1 Q). by rewrite (filtergtn_LRsupport HLR) -{1}(shaped_hyper_stdtabnP P1) /=. set t := map _ _. have -> : shape Q = outer_shape (shape (filter_gt_tab d1 Q)) (shape t). rewrite /outer_shape /= {}/t. have:= stdtabP (stdtabnP Q) => /(join_tab_filter d1) {1}<-. rewrite /= /shape /join_tab /pad /=. rewrite !size_map -map_comp. rewrite (eq_map (g := fun p => size p.1 + size p.2)); first last. by move=> i /=; rewrite size_cat. rewrite size_zip2; congr (map _ (zip _ _)). move: (size Q) => n. elim: (filter _ _) n => [// | t0 t IHt] n /=; first by rewrite map_nseq. case: n => [| n] /=; first by rewrite !cats0. by rewrite subSS IHt. apply skew_reshapeK. rewrite /t /= /shape !size_map size_filter. apply (leq_trans (count_size _ _)). by rewrite size_map. 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