CoqEAL multipoly — multivariate polynomials as finite maps

CoqEAL's multipoly refines multivariate polynomials to finite maps from monomial exponent vectors to coefficients. In Mathlib MvPolynomial σ R is such a finite map (σ →₀ ℕ exponents to coefficients), so the refinement is exhibited by reading coefficients: a monomial's exponent vector selects its coefficient. This file pins that reading down on X and on a monomial, the base of the multipoly representation; the arithmetic refinement (coeff_mul over the exponent antidiagonal) is the suite's frontier.