proposition: Lemma catlangM d1 d2 (s1 : homlang d1) (s2 : homlang d2) : polylang s1 * polylang s2 = polylang (catlang s1 s2).
proof: Proof. Proof using . rewrite /polylang /catlang mulr_suml. under eq_bigr do [rewrite mulr_sumr; under eq_bigr do rewrite -commword_morph]. rewrite pair_big /=. rewrite -(big_imset (h := fun p => cat_tuple p.1 p.2) commword) /=; last by move=> [u v] [x y] /= _ _; apply: cat_tuple_inj. apply: eq_bigl => w. apply/idP/idP. - move/imsetP => [] [u v] /=; rewrite unfold_in /= => /andP[Hu Hv] ->. exact: imset2_f. - move/imset2P => [u v Hu Hv -> {w}]. by apply/imsetP; exists (u, v) => //=; rewrite unfold_in /= Hu Hv. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(ssrcomplements freeg mpoly) tools ordtype partition Yamanouchi std tableau stdtab Schensted congr plactic stdplact Yam_plact Greene_inv shuffle Schur_mpoly