no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q p : R[X]
hq : q ≠ 0
hp : p = 0
⊢ degree p ≤ degree (p * q)
simp only [hp, MulZeroClass.zero_mul, le_refl]
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q p : R[X]
hq : q ≠ 0
hp : ¬p = 0
⊢ ↑(natDegree p) ≤ ↑(natDegree p) + ↑(natDegree q)
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q p : R[X]
hq : q ≠ 0
hp : ¬p = 0
⊢ degree p ≤ degree (p * q)
rw [degree_mul, degree_eq_natDegree hp, degree_eq_natDegree hq]
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q p : R[X]
hq : q ≠ 0
hp : ¬p = 0
⊢ ↑(natDegree p) ≤ ↑(natDegree p) + ↑(natDegree q)
exact WithBot.coe_le_coe.2 (Nat.le_add_right _ _)