case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : q = 0
⊢ natDegree (p * q) < natDegree p ↔ p ≠ 1 ∧ q = 0

case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : ¬q = 0
⊢ natDegree (p * q) < natDegree p ↔ p ≠ 1 ∧ q = 0
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
⊢ natDegree (p * q) < natDegree p ↔ p ≠ 1 ∧ q = 0
by_cases hq : q = 0
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : q = 0
⊢ 0 < natDegree p ↔ natDegree p ≠ 0
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : q = 0
⊢ natDegree (p * q) < natDegree p ↔ p ≠ 1 ∧ q = 0
suffices 0 < p.natDegree ↔ p.natDegree ≠ 0 by simpa [hq, ← h.natDegree_eq_zero_iff_eq_one]
no goals
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : q = 0
⊢ 0 < natDegree p ↔ natDegree p ≠ 0
exact ⟨fun h => h.ne', fun h => lt_of_le_of_ne (Nat.zero_le _) h.symm⟩
no goals
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : q = 0
this : 0 < natDegree p ↔ natDegree p ≠ 0
⊢ natDegree (p * q) < natDegree p ↔ p ≠ 1 ∧ q = 0
simpa [hq, ← h.natDegree_eq_zero_iff_eq_one]
no goals
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
h : Monic p
q : R[X]
hq : ¬q = 0
⊢ natDegree (p * q) < natDegree p ↔ p ≠ 1 ∧ q = 0
simp [h.natDegree_mul', hq]