∀ {n : ℕ} (a : Composition n) (b : Composition a.length) (i : Fin (a.gather b).length),
  a.sigmaCompositionAux b i = { blocks := (a.blocks.splitWrtComposition b)[↑i], blocks_pos := ⋯, blocks_sum := ⋯ }