proposition: Fact join_YoungP sh1 sh2 sh : (join_Young sh1 sh2 <= sh)%O = (sh1 <= sh)%O && (sh2 <= sh)%O.
proof: Proof. apply/idP/andP => [Hsup |]. split; apply: (le_trans _ Hsup); first exact: join_Young_le. by rewrite join_YoungC join_Young_le. move=> [/le_YoungP le1 /le_YoungP le2]. by apply/le_YoungP => i; rewrite nth_join_Young geq_max le1 le2. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype