R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p ≠ 0
q : R[X]
this : degree (gcd p q) ≤ ↑(natDegree p)
⊢ degree (gcd p q) ≤ degree p
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p ≠ 0
q : R[X]
⊢ degree (gcd p q) ≤ degree p
have := natDegree_le_iff_degree_le.mp (natDegree_le_of_dvd (gcd_dvd_left p q) hp)
no goals
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
hp : p ≠ 0
q : R[X]
this : degree (gcd p q) ≤ ↑(natDegree p)
⊢ degree (gcd p q) ≤ degree p
rwa [degree_eq_natDegree hp]