R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hp : Monic p
hpq : degree q < degree p
⊢ Monic (p + -q)
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hp : Monic p
hpq : degree q < degree p
⊢ Monic (p - q)
rw [sub_eq_add_neg]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hp : Monic p
hpq : degree q < degree p
⊢ degree (-q) < degree p
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hp : Monic p
hpq : degree q < degree p
⊢ Monic (p + -q)
apply hp.add_of_left
no goals
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hp : Monic p
hpq : degree q < degree p
⊢ degree (-q) < degree p
rwa [degree_neg]