chore(representation_theory/group_cohomology): use `fin.cast_succ` instead of coe (#18950)
This replaces the cast from `fin n` to `fin (n + 1)` (defined as `⟨↑i % (n + 1), _⟩`) with `fin.cast_succ` (defined as `⟨↑i, _⟩`).
This is the preferred spelling, and using it lets us simplify some proofs.
This also removes the `g` argument from `partial_prod_right_inv`, as it was not used, and the interesting statement is the one without it.