Single-box interpolation for Young diagrams

Given lam ≤ mu with lam.card < mu.card, we produce nu satisfying lam ≤ nu ≤ mu and nu.card = lam.card + 1. The idea is to pick a cell in mu.cells \ lam.cells that is minimal for the sum of coordinates, then insert it into lam.

theorem RS.exists_intermediate_diagram {lam mu : YoungDiagram} (hle : lam ≤ mu) (hlt : lam.card < mu.card) : ∃ (nu : YoungDiagram), lam ≤ nu ∧ nu ≤ mu ∧ nu.card = lam.card + 1

Single-box interpolation: a strictly larger diagram can be reached one cell at a time.