R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p q : R[X]
h : degree q ≤ degree p ∧ p ≠ 0
hq : Monic q
hp : leadingCoeff p ≠ 0
hq0 : q ≠ 0
⊢ degree q ≤ degree p
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p q : R[X]
h : degree q ≤ degree p ∧ p ≠ 0
hq : Monic q
hp : leadingCoeff p ≠ 0
hq0 : q ≠ 0
⊢ ↑(natDegree q) ≤ ↑(natDegree p)
rw [← Nat.cast_withBot, ← Nat.cast_withBot, ← degree_eq_natDegree h.2,
← degree_eq_natDegree hq0]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p q : R[X]
h : degree q ≤ degree p ∧ p ≠ 0
hq : Monic q
hp : leadingCoeff p ≠ 0
hq0 : q ≠ 0
⊢ degree q ≤ degree p
exact h.1
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p q : R[X]
h : degree q ≤ degree p ∧ p ≠ 0
hq : Monic q
hp : leadingCoeff p ≠ 0
hq0 : q ≠ 0
hlt : natDegree q ≤ natDegree p
⊢ degree p = degree (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q)
rw [hq.degree_mul, degree_C_mul_X_pow _ hp, degree_eq_natDegree h.2,
  degree_eq_natDegree hq0, ← Nat.cast_add, tsub_add_cancel_of_le hlt]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p q : R[X]
h : degree q ≤ degree p ∧ p ≠ 0
hq : Monic q
hp : leadingCoeff p ≠ 0
hq0 : q ≠ 0
hlt : natDegree q ≤ natDegree p
⊢ leadingCoeff p = leadingCoeff (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q)
rw [leadingCoeff_mul_monic hq, leadingCoeff_mul_X_pow, leadingCoeff_C]