∀ {R : Type u_1} [inst : CommRing R] (N : ℕ) {F : MvPolynomial (Fin (N + 1)) R} {n : ℕ},
  ((MvPolynomial.finSuccEquiv R N) F).natDegree < n + 1 →
    ((MvPolynomial.finSuccEquiv R N) F).natDegree ≠ n → ((MvPolynomial.finSuccEquiv R N) F).natDegree < n