Row lengths along single-box extensions

A diagram extending another by a single cell bumps exactly one row length by one; row lengths are monotone in diagram containment.

theorem RS.rowLen_mono {lam mu : YoungDiagram} (hle : lam ≤ mu) (i : ℕ) : lam.rowLen i ≤ mu.rowLen i

Row lengths are monotone in diagram containment.

theorem RS.rowLen_of_card_succ {lam nu : YoungDiagram} (hle : lam ≤ nu) (hcard : nu.card = lam.card + 1) : ∃ (i₀ : ℕ), ∀ (i : ℕ), nu.rowLen i = if i = i₀ then lam.rowLen i + 1 else lam.rowLen i

A single-cell extension bumps exactly one row length.