proposition: Lemma size_join_Young p q : size (p `|` q)%O = maxn (size p) (size q).
proof: Proof. exact: size_join_Young. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype