R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.1058825
ha : a ≠ 0
⊢ ↑2 = 2
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.1058825
ha : a ≠ 0
⊢ degree (↑C a * X ^ 2 + ↑C b * X + ↑C c) = 2
rw [add_assoc, degree_add_eq_left_of_degree_lt <| degree_linear_lt_degree_C_mul_X_sq ha,
  degree_C_mul_X_pow 2 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.1058825
ha : a ≠ 0
⊢ ↑2 = 2
rfl