Implement finSuccEquiv and optionEquivLeft for CMvPolynomial

[dhsorens]

Implement the variable manipulation equivalences for CMvPolynomial:

• finSuccEquiv: Equivalence between CMvPolynomial (n+1) R and polynomials in one variable over CMvPolynomial n R (analogous to Mathlib's MvPolynomial.finSuccEquiv).
• optionEquivLeft: Equivalence for option-indexed variables (analogous to Mathlib's MvPolynomial.optionEquivLeft).

TODOs exist in CMvPolynomial.lean (lines ~295-296). Listed in ROADMAP.md Phase 1 under "Variable manipulation equivalences".