∀ {n : ℕ} (a : Composition n) (b : Composition a.length) {i j : ℕ} (hi : i < b.length),
  j < b.blocksFun ⟨i, hi⟩ →
    a.sizeUpTo (b.sizeUpTo i + j) = (a.gather b).sizeUpTo i + (a.sigmaCompositionAux b ⟨i, ⋯⟩).sizeUpTo j