proposition: Lemma size_join_Young sh1 sh2 : size (join_Young_fun sh1 sh2) = maxn (size sh1) (size sh2).
proof: Proof. rewrite size_map size_zip !size_cat !size_nseq. by rewrite !subnKC ?leq_maxl ?leq_maxr // minnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype