proposition: Lemma shiftn_skew_dominate n sh u v : skew_dominate sh u v -> skew_dominate sh (shiftn n u) (shiftn n v).
proof: Proof. rewrite /skew_dominate /dominate !size_map => /andP[Hsz]. rewrite -map_drop size_map Hsz /=. set p1 := (X in all X) => H. set p2 := (X in all X). rewrite (eq_in_all (a2 := p1)) //=. move => i /=; rewrite mem_iota add0n => /= Hi1. case (leqP sh (size u)) => Hu. + rewrite {H}/p1 {}/p2 /shiftn. rewrite !ltEnat /= (nth_map inh _ _ (leq_trans Hi1 Hsz)) (nth_map inh _ _ Hi1). by rewrite ltn_add2l. + exfalso; move: Hi1; rewrite size_drop. move: Hu => /ltnW; rewrite {1}/leq => /eqP ->. by rewrite ltn0. 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