proposition: Lemma nth_meet_Young sh1 sh2 i : nth 0 (meet_Young_fun sh1 sh2) i = minn (nth 0 sh1 i) (nth 0 sh2 i).
proof: Proof. rewrite /meet_Young_fun /=. case: (ltnP i (size (zip sh1 sh2))) => Hi. by rewrite (nth_map (0, 0) _ _ Hi) /= nth_zip_cond Hi. rewrite [LHS]nth_default ?size_map //; apply/esym/eqP; rewrite -leqn0. move: Hi; rewrite size_zip geq_min. by move/orP => []/(nth_default _) ->; rewrite ?minn0 ?min0n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype