proposition: Fact meet_Young_subproof sh1 sh2 : is_part (meet_Young_fun sh1 sh2).
proof: Proof. rewrite is_part_sortedE; apply/andP; split; first last. apply/negP => /(nthP 0) [i]; rewrite nth_meet_Young. rewrite size_meet_Young ltn_min => /andP[le1 le2] /eqP. rewrite -leqn0 geq_min. by move=> /orP[]; rewrite leqn0; apply/negP; rewrite nth_part_non0 //. apply/(sortedP 0) => i _ /=. rewrite !nth_meet_Young !leq_min !geq_min. 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