case a
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.695041
p q : R[X]
⊢ degree (p * q) ≤ ↑(natDegree p + natDegree q)
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.695041
p q : R[X]
⊢ natDegree (p * q) ≤ natDegree p + natDegree q
apply natDegree_le_of_degree_le
case a
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.695041
p q : R[X]
⊢ degree p + degree q ≤ ↑(natDegree p + natDegree q)
case a
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.695041
p q : R[X]
⊢ degree (p * q) ≤ ↑(natDegree p + natDegree q)
apply le_trans (degree_mul_le p q)
case a
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.695041
p q : R[X]
⊢ degree p + degree q ≤ ↑(natDegree p) + ↑(natDegree q)
case a
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.695041
p q : R[X]
⊢ degree p + degree q ≤ ↑(natDegree p + natDegree q)
rw [Nat.cast_withBot, WithBot.coe_add]
no goals
case a
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.695041
p q : R[X]
⊢ degree p + degree q ≤ ↑(natDegree p) + ↑(natDegree q)
refine' add_le_add _ _ <;> apply degree_le_natDegree