R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
hp0 : p ≠ 0
h0q : 0 < degree q
hpq : degree p < degree q
this : Nontrivial R
⊢ degree (p /ₘ q) < degree p
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
hp0 : p ≠ 0
h0q : 0 < degree q
hpq : degree p < degree q
⊢ degree (p /ₘ q) < degree p
haveI := Nontrivial.of_polynomial_ne hp0
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
hp0 : p ≠ 0
h0q : 0 < degree q
hpq : degree p < degree q
this : Nontrivial R
⊢ degree 0 < ↑(natDegree p)
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
hp0 : p ≠ 0
h0q : 0 < degree q
hpq : degree p < degree q
this : Nontrivial R
⊢ degree (p /ₘ q) < degree p
rw [(divByMonic_eq_zero_iff hq).2 hpq, degree_eq_natDegree hp0]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
hp0 : p ≠ 0
h0q : 0 < degree q
hpq : degree p < degree q
this : Nontrivial R
⊢ degree 0 < ↑(natDegree p)
exact WithBot.bot_lt_coe _
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
hp0 : p ≠ 0
h0q : 0 < degree q
hpq : ¬degree p < degree q
this : Nontrivial R
⊢ degree (p /ₘ q) < degree p
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
hp0 : p ≠ 0
h0q : 0 < degree q
hpq : ¬degree p < degree q
⊢ degree (p /ₘ q) < degree p
haveI := Nontrivial.of_polynomial_ne hp0
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
hp0 : p ≠ 0
h0q : 0 < degree q
hpq : ¬degree p < degree q
this : Nontrivial R
⊢ ↑(natDegree (p /ₘ q)) < ↑(natDegree q) + ↑(natDegree (p /ₘ q))
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
hp0 : p ≠ 0
h0q : 0 < degree q
hpq : ¬degree p < degree q
this : Nontrivial R
⊢ degree (p /ₘ q) < degree p
rw [← degree_add_divByMonic hq (not_lt.1 hpq), degree_eq_natDegree hq.ne_zero,
  degree_eq_natDegree (mt (divByMonic_eq_zero_iff hq).1 hpq)]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
hp0 : p ≠ 0
h0q : 0 < degree q
hpq : ¬degree p < degree q
this : Nontrivial R
⊢ ↑(natDegree (p /ₘ q)) < ↑(natDegree q) + ↑(natDegree (p /ₘ q))
exact
  WithBot.coe_lt_coe.2
    (Nat.lt_add_of_pos_left (WithBot.coe_lt_coe.1 <|
      by simpa [Nat.cast_withBot, degree_eq_natDegree hq.ne_zero] using h0q))
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hq : Monic q
hp0 : p ≠ 0
h0q : 0 < degree q
hpq : ¬degree p < degree q
this : Nontrivial R
⊢ ↑0 < ↑↑(natDegree q)
simpa [Nat.cast_withBot, degree_eq_natDegree hq.ne_zero] using h0q