diff --git a/CompPoly.lean b/CompPoly.lean
index 95805bdc..ba204b71 100644
--- a/CompPoly.lean
+++ b/CompPoly.lean
@@ -1,55 +1,56 @@
+import CompPoly.Bivariate.Basic
+import CompPoly.Bivariate.ToPoly
 import CompPoly.Data.Array.Lemmas
 import CompPoly.Data.Classes.DCast
 import CompPoly.Data.Fin.BigOperators
 import CompPoly.Data.List.Lemmas
+import CompPoly.Data.MvPolynomial.Notation
 import CompPoly.Data.Nat.Bitwise
 import CompPoly.Data.Polynomial.Frobenius
-import CompPoly.Data.MvPolynomial.Notation
+import CompPoly.Data.Polynomial.MonomialBasis
 import CompPoly.Data.RingTheory.AlgebraTower
 import CompPoly.Data.RingTheory.CanonicalEuclideanDomain
 import CompPoly.Data.Vector.Basic
+import CompPoly.Fields.BLS12_377
+import CompPoly.Fields.BLS12_381
+import CompPoly.Fields.BN254
+import CompPoly.Fields.BabyBear
+import CompPoly.Fields.Basic
+import CompPoly.Fields.Binary.AdditiveNTT.AdditiveNTT
+import CompPoly.Fields.Binary.AdditiveNTT.Impl
+import CompPoly.Fields.Binary.AdditiveNTT.NovelPolynomialBasis
+import CompPoly.Fields.Binary.BF128Ghash.Basic
+import CompPoly.Fields.Binary.BF128Ghash.Impl
+import CompPoly.Fields.Binary.BF128Ghash.Prelude
+import CompPoly.Fields.Binary.BF128Ghash.XPowTwoPowGcdCertificate
+import CompPoly.Fields.Binary.BF128Ghash.XPowTwoPowModCertificate
+import CompPoly.Fields.Binary.Common
+import CompPoly.Fields.Binary.Tower.Basic
+import CompPoly.Fields.Binary.Tower.Impl
+import CompPoly.Fields.Binary.Tower.Prelude
+import CompPoly.Fields.Binary.Tower.TensorAlgebra
+import CompPoly.Fields.Goldilocks
+import CompPoly.Fields.KoalaBear
+import CompPoly.Fields.Mersenne
+import CompPoly.Fields.PrattCertificate
+import CompPoly.Fields.Secp256k1
 import CompPoly.Multilinear.Basic
 import CompPoly.Multilinear.Equiv
 import CompPoly.Multivariate.CMvMonomial
 import CompPoly.Multivariate.CMvPolynomial
 import CompPoly.Multivariate.CMvPolynomialEvalLemmas
-import CompPoly.Multivariate.Restrict
-import CompPoly.Multivariate.VarsDegrees
 import CompPoly.Multivariate.Lawful
 import CompPoly.Multivariate.MvPolyEquiv
 import CompPoly.Multivariate.Rename
+import CompPoly.Multivariate.Restrict
 import CompPoly.Multivariate.Unlawful
+import CompPoly.Multivariate.VarsDegrees
 import CompPoly.Multivariate.Wheels
-import CompPoly.Univariate.Raw
+import CompPoly.ToMathlib.Finsupp.Fin
+import CompPoly.ToMathlib.MvPolynomial.Equiv
 import CompPoly.Univariate.Basic
+import CompPoly.Univariate.Lagrange
 import CompPoly.Univariate.Quotient
-import CompPoly.Univariate.ToPoly
 import CompPoly.Univariate.QuotientEquiv
-import CompPoly.Univariate.Lagrange
-import CompPoly.Bivariate.Basic
-import CompPoly.Bivariate.ToPoly
-import CompPoly.ToMathlib.Finsupp.Fin
-import CompPoly.ToMathlib.MvPolynomial.Equiv
-import CompPoly.Fields.Basic
-import CompPoly.Fields.BabyBear
-import CompPoly.Fields.Binary.AdditiveNTT.NovelPolynomialBasis
-import CompPoly.Fields.Binary.AdditiveNTT.AdditiveNTT
-import CompPoly.Fields.Binary.AdditiveNTT.Impl
-import CompPoly.Fields.Binary.Common
-import CompPoly.Fields.Binary.Tower.Prelude
-import CompPoly.Fields.Binary.Tower.Basic
-import CompPoly.Fields.Binary.Tower.Impl
-import CompPoly.Fields.Binary.Tower.TensorAlgebra
-import CompPoly.Fields.Binary.BF128Ghash.Prelude
-import CompPoly.Fields.Binary.BF128Ghash.XPowTwoPowModCertificate
-import CompPoly.Fields.Binary.BF128Ghash.XPowTwoPowGcdCertificate
-import CompPoly.Fields.Binary.BF128Ghash.Basic
-import CompPoly.Fields.Binary.BF128Ghash.Impl
-import CompPoly.Fields.BLS12_377
-import CompPoly.Fields.BLS12_381
-import CompPoly.Fields.BN254
-import CompPoly.Fields.Goldilocks
-import CompPoly.Fields.KoalaBear
-import CompPoly.Fields.Mersenne
-import CompPoly.Fields.Secp256k1
-import CompPoly.Fields.PrattCertificate
+import CompPoly.Univariate.Raw
+import CompPoly.Univariate.ToPoly
diff --git a/CompPoly/Data/MvPolynomial/FirstVarsDegree.lean b/CompPoly/Data/MvPolynomial/FirstVarsDegree.lean
new file mode 100644
index 00000000..45a17bd7
--- /dev/null
+++ b/CompPoly/Data/MvPolynomial/FirstVarsDegree.lean
@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2025 CompPoly. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Elias Judin
+-/
+
+import Mathlib.Algebra.MvPolynomial.Basic
+import Mathlib.Data.Finsupp.Fin
+
+/-!
+# First-variable degree helpers for `MvPolynomial (Fin (n + 1)) R`
+
+This file defines the maximal total degree contributed by the first `n` variables
+(i.e., all variables except the last coordinate).
+-/
+
+namespace MvPolynomial
+
+open Finsupp
+
+section FirstVarsDegree
+
+variable {n : ℕ} {R : Type*} [CommSemiring R]
+
+/-- Maximal degree contributed by the first `n` variables of a polynomial on `Fin (n + 1)`.
+
+This is the support supremum of the sum of coordinates on `Fin.castSucc`. -/
+noncomputable def firstVarsDegree (P : MvPolynomial (Fin (n + 1)) R) : ℕ :=
+  P.support.sup (fun α => ∑ i : Fin n, α (Fin.castSucc i))
+
+/-- A support element bounds `firstVarsDegree` from below. -/
+lemma le_firstVarsDegree_of_mem_support {P : MvPolynomial (Fin (n + 1)) R}
+    {α : Fin (n + 1) →₀ ℕ} (hα : α ∈ P.support) :
+    (∑ i : Fin n, α (Fin.castSucc i)) ≤ firstVarsDegree (R := R) P := by
+  classical
+  simpa using Finset.le_sup (s := P.support)
+    (f := fun β : Fin (n + 1) →₀ ℕ => ∑ i : Fin n, β (Fin.castSucc i)) hα
+
+/-- `firstVarsDegree` of a monomial with nonzero coefficient. -/
+lemma firstVarsDegree_monomial (α : Fin (n + 1) →₀ ℕ) (c : R) (hc : c ≠ 0) :
+    firstVarsDegree (R := R) (MvPolynomial.monomial α c) =
+      (∑ i : Fin n, α (Fin.castSucc i)) := by
+  classical
+  have hsupp : (MvPolynomial.monomial α c).support = {α} := by
+    rw [MvPolynomial.support_monomial, if_neg hc]
+  simp [firstVarsDegree, hsupp]
+
+end FirstVarsDegree
+
+end MvPolynomial
diff --git a/CompPoly/ToMathlib/MvPolynomial/Equiv.lean b/CompPoly/ToMathlib/MvPolynomial/Equiv.lean
index f3f1e99a..3a33c69a 100644
--- a/CompPoly/ToMathlib/MvPolynomial/Equiv.lean
+++ b/CompPoly/ToMathlib/MvPolynomial/Equiv.lean
@@ -1,10 +1,11 @@
 /-
 Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Chung Thai Nguyen, Quang Dao
+Authors: Chung Thai Nguyen, Quang Dao, Elias Judin
 -/
 
 import Mathlib.Algebra.MvPolynomial.Equiv
+import CompPoly.Data.MvPolynomial.FirstVarsDegree
 import CompPoly.ToMathlib.Finsupp.Fin
 
 /-!
@@ -224,6 +225,19 @@ theorem degreeOf_coeff_finSuccEquivNth (f : MvPolynomial (Fin (n + 1)) R) (j : F
   exact Finset.le_sup (f := fun (g : Fin n.succ →₀ ℕ) => g (Fin.succAbove p j))
     (support_coeff_finSuccEquivNth.1 hm)
 
+
+/-- Coefficient in the last variable after `finSuccEquiv`. -/
+noncomputable def leadingCoeffFinSucc (P : MvPolynomial (Fin (n + 1)) R)
+    (d : ℕ) : MvPolynomial (Fin n) R :=
+  (MvPolynomial.finSuccEquiv R n P).coeff d
+
+/-- Coefficients of `leadingCoeffFinSucc` are the corresponding coefficients of `P`. -/
+@[simp] lemma coeff_leadingCoeffFinSucc (P : MvPolynomial (Fin (n + 1)) R)
+    (d : ℕ) (i : Fin n →₀ ℕ) :
+    (leadingCoeffFinSucc (R := R) P d).coeff i = P.coeff (i.cons d) := by
+  simpa [leadingCoeffFinSucc] using
+    (MvPolynomial.finSuccEquiv_coeff_coeff (f := P) (m := i) (i := d))
+
 /-- Consider a multivariate polynomial `φ` whose variables are indexed by `Option σ`,
 and suppose that `σ ≃ Fin n`.
 Then one may view `φ` as a polynomial over `MvPolynomial (Fin n) R`, by