proposition: Lemma is_skew_tableau_map_shiftn sh inn t : is_skew_tableau inn t -> is_skew_tableau inn (map (shiftn sh) t).
proof: Proof. elim: t inn => [// | r0 t IHt] /= inn. move=> /and4P[Hszr0 Hrow0 Hdom Hskew]. apply/and4P; split. - by rewrite size_map. - rewrite /shiftn. case: r0 Hrow0 {Hdom Hskew IHt Hszr0} => [// | l0 r] /= H. rewrite (map_path (e' := <=%O) (b := pred0)). + exact: H. + by move=> i j /= _; rewrite !leEnat leq_add2l. + by apply/hasPn => i. - have -> : head [::] (map (shiftn sh) t) = shiftn sh (head [::] t) by case t. exact: shiftn_skew_dominate. - exact: 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