R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hq : Polynomial.leadingCoeff q = -1
hpq : degree p < degree q
this : coeff (-q) (natDegree (-q)) = 1
⊢ Monic (p - q)
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hq : Polynomial.leadingCoeff q = -1
hpq : degree p < degree q
⊢ Monic (p - q)
have : (-q).coeff (-q).natDegree = 1 := by
  rw [natDegree_neg, coeff_neg, show q.coeff q.natDegree = -1 from hq, neg_neg]
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hq : Polynomial.leadingCoeff q = -1
hpq : degree p < degree q
this : coeff (-q) (natDegree (-q)) = 1
⊢ Monic (p + -q)
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hq : Polynomial.leadingCoeff q = -1
hpq : degree p < degree q
this : coeff (-q) (natDegree (-q)) = 1
⊢ 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]
hq : Polynomial.leadingCoeff q = -1
hpq : degree p < degree q
this : coeff (-q) (natDegree (-q)) = 1
⊢ degree p < degree (-q)
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hq : Polynomial.leadingCoeff q = -1
hpq : degree p < degree q
this : coeff (-q) (natDegree (-q)) = 1
⊢ Monic (p + -q)
apply Monic.add_of_right this
no goals
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hq : Polynomial.leadingCoeff q = -1
hpq : degree p < degree q
this : coeff (-q) (natDegree (-q)) = 1
⊢ degree p < degree (-q)
rwa [degree_neg]
no goals
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Ring R
p✝ p q : R[X]
hq : Polynomial.leadingCoeff q = -1
hpq : degree p < degree q
⊢ coeff (-q) (natDegree (-q)) = 1
rw [natDegree_neg, coeff_neg, show q.coeff q.natDegree = -1 from hq, neg_neg]