feat: reflections, inversion sequences in Coxeter groups

[trivial1711]

• Add theorem List.length_eraseIdx_add_one to Data/List/Basic.lean, which states that if i < l.length, then the length of l.eraseIdx i plus one is equal to the length of l.
• Add new file GroupTheory/Coxeter/Inversion.lean. Define reflections, left inversions, right inversions, and inversion sequences. Prove their basic properties.

I decided to split #11408 (now closed) into two pull requests. This is the second one. The first is #11465.

---

• [x] depends on: #11465

[trivial1711]

I'm not entirely sure what happened with the CI here. It is not very clear about what went wrong.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#11465~~ By Dependent Issues (🤖). Happy coding!

[trivial1711]

Thank you so much for the feedback.

[jcommelin]

bors d+

[mathlib-bors[bot]]

:v: trivial1711 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[trivial1711]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style