no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
ι : Type ?u.511565
p q : R[X]
⊢ natDegree (p + q) ≤ max (natDegree p) (natDegree q)
cases' le_max_iff.1 (degree_add_le p q) with h h <;> simp [natDegree_le_natDegree h]