proposition: Lemma join_YoungC : commutative join_Young.
proof: Proof. move=> sh1 sh2; apply/eqP/intpart_eqP => i. by rewrite !nth_join_Young maxnC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype