R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q✝ p q : R[X]
h0 : q ≠ 0
hl : natDegree q < natDegree p
hcontra : p ∣ q
⊢ False
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q✝ p q : R[X]
h0 : q ≠ 0
hl : natDegree q < natDegree p
⊢ ¬p ∣ q
by_contra hcontra
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p✝ q✝ p q : R[X]
h0 : q ≠ 0
hl : natDegree q < natDegree p
hcontra : p ∣ q
⊢ False
exact h0 (eq_zero_of_dvd_of_natDegree_lt hcontra hl)