R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
h : degree p < degree (-q)
⊢ degree (p - q) = degree q
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
h : degree p < degree q
⊢ degree (p - q) = degree q
rw [← degree_neg q] at h
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Ring R
p q : R[X]
h : degree p < degree (-q)
⊢ degree (p - q) = degree q
rw [sub_eq_add_neg, degree_add_eq_right_of_degree_lt h, degree_neg]