proposition: Lemma size_zip2 (T : Type) (s t : seq (seq T)) : [seq size p.1 + size p.2 | p <- zip s t] = [seq p.1 + p.2 | p <- zip (map size s) (map size t)].
proof: Proof. Proof using . elim: s t => [| s0 s IHs] /=; first by elim=> [| t0 t IHt]. case=> [// | t0 t] /=. by rewrite -IHs. 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