R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.707375
hp : p ≠ 0
this : Nontrivial R
⊢ degree p < degree (p * X)
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.707375
hp : p ≠ 0
⊢ degree p < degree (p * X)
haveI := Nontrivial.of_polynomial_ne hp
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.707375
hp : p ≠ 0
this✝ : Nontrivial R
this : leadingCoeff p * leadingCoeff X ≠ 0
⊢ degree p < degree (p * X)
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.707375
hp : p ≠ 0
this : Nontrivial R
⊢ degree p < degree (p * X)
have : leadingCoeff p * leadingCoeff X ≠ 0 := by simpa
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.707375
hp : p ≠ 0
this✝ : Nontrivial R
this : leadingCoeff p * leadingCoeff X ≠ 0
⊢ ↑(natDegree p) < ↑(natDegree p) + 1
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.707375
hp : p ≠ 0
this✝ : Nontrivial R
this : leadingCoeff p * leadingCoeff X ≠ 0
⊢ degree p < degree (p * X)
erw [degree_mul' this, degree_eq_natDegree hp, degree_X, ← WithBot.coe_one,
  ← WithBot.coe_add, WithBot.coe_lt_coe]
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.707375
hp : p ≠ 0
this✝ : Nontrivial R
this : leadingCoeff p * leadingCoeff X ≠ 0
⊢ ↑(natDegree p) < ↑(natDegree p) + 1
exact Nat.lt_succ_self _
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.707375
hp : p ≠ 0
this : Nontrivial R
⊢ leadingCoeff p * leadingCoeff X ≠ 0
simpa