proposition: Lemma nth_join_Young sh1 sh2 i : nth 0 (join_Young_fun sh1 sh2) i = maxn (nth 0 sh1 i) (nth 0 sh2 i).
proof: Proof. case: (ltnP i (size (join_Young_fun sh1 sh2))) => Hi; first last. by rewrite !nth_default // (leq_trans _ Hi) // size_join_Young ?leq_maxl ?leq_maxr. have := Hi; rewrite /join_Young_fun size_map => /= Hi1. rewrite (nth_map (0, 0)) // {Hi1}. rewrite !nth_zip /=; first last. by rewrite !size_cat !size_nseq -!maxnE maxnA maxnn [RHS]maxnC -maxnA maxnn. rewrite !nth_cat !nth_nseq !if_same. by rewrite !if_nth // orbC leqVgt. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype