Complete summable FPS coefficient and Fubini rules

[faabian]

Completes two clauses of the raw TeX statements that were not represented by the existing API.

• Adds the arbitrary determining-finset coefficient formula from Proposition prop.fps.summable=fin-det(b).
• Proves summability of the families of row and column sums under product-indexed summability.
• Adds the full discrete Fubini equality between the row-iterated, product-indexed, and column-iterated sums from Proposition prop.fps.summable-sums-rule.
• Retains arbitrary index types and CommRing coefficients.

The proof is coefficientwise and reduces finsums to a finite rectangle containing the support.

Validation:

• lake build AlgebraicCombinatorics.FPSDefinition
• lake build (8078 jobs; successful; only pre-existing sorry warnings in unrelated files)