R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.1382528
ha : a ≠ 0
⊢ ↑3 = 3
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.1382528
ha : a ≠ 0
⊢ degree (↑C a * X ^ 3 + ↑C b * X ^ 2 + ↑C c * X + ↑C d) = 3
rw [add_assoc, add_assoc, ← add_assoc (C b * X ^ 2),
  degree_add_eq_left_of_degree_lt <| degree_quadratic_lt_degree_C_mul_X_cb ha,
  degree_C_mul_X_pow 3 ha]
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.1382528
ha : a ≠ 0
⊢ ↑3 = 3
rfl