proposition: Fact join_Young_subproof sh1 sh2 : is_part (join_Young_fun sh1 sh2).
proof: Proof. rewrite is_part_sortedE; apply/andP; split; first last. apply/negP => /(nthP 0) [i]; rewrite nth_join_Young. rewrite size_join_Young leq_max. by move=> /orP[] /(nth_part_non0 (intpartP _)) Hi /eqP; rewrite -leqn0 geq_max !leqn0 (negbTE Hi) ?andbF //. apply/(sortedP 0) => i _ /=. rewrite !nth_join_Young !geq_max !leq_max. have /is_partP[_ -> /=]:= intpartP sh1. have /is_partP[_ -> /=]:= intpartP sh2. by rewrite orbT. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype