no goals
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
h : X ^ n + ↑C a = 1
⊢ n = 0
simpa only [natDegree_X_pow_add_C, natDegree_one] using congr_arg natDegree h