case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p r✝ : R[X]
hp : Monic p
r : R[X]
h0 : p * r ≠ 0
hl : natDegree (p * r) < natDegree p
⊢ False
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h0 : q ≠ 0
hl : natDegree q < natDegree p
⊢ ¬p ∣ q
rintro ⟨r, rfl⟩
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p r✝ : R[X]
hp : Monic p
r : R[X]
h0 : p * r ≠ 0
hl : natDegree p + natDegree r < natDegree p
⊢ False
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p r✝ : R[X]
hp : Monic p
r : R[X]
h0 : p * r ≠ 0
hl : natDegree (p * r) < natDegree p
⊢ False
rw [hp.natDegree_mul' <| right_ne_zero_of_mul h0] at hl
no goals
case intro
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p r✝ : R[X]
hp : Monic p
r : R[X]
h0 : p * r ≠ 0
hl : natDegree p + natDegree r < natDegree p
⊢ False
exact hl.not_le (Nat.le_add_right _ _)