∀ {R : Type u} [inst : CommSemiring R] {n : ℕ} (m : Fin n →₀ ℕ) (f : MvPolynomial (Fin (n + 1)) R) (i : ℕ),
  MvPolynomial.coeff (Finsupp.cons i m) f = MvPolynomial.coeff m (((MvPolynomial.finSuccEquiv R n) f).coeff i)