R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
⊢ degree (divX p) < degree p
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
⊢ degree (divX p) < degree p
haveI := Nontrivial.of_polynomial_ne hp0
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
⊢ degree (divX p) < degree p
calc
  degree (divX p) < (divX p * X + C (p.coeff 0)).degree :=
    if h : degree p ≤ 0 then by
      have h' : C (p.coeff 0) ≠ 0 := by rwa [← eq_C_of_degree_le_zero h]
      rw [eq_C_of_degree_le_zero h, divX_C, degree_zero, zero_mul, zero_add]
      exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 <| by simpa using h'))
    else by
      have hXp0 : divX p ≠ 0 := by
        simpa [divX_eq_zero_iff, -not_le, degree_le_zero_iff] using h
      have : leadingCoeff (divX p) * leadingCoeff X ≠ 0 := by simpa
      have : degree (C (p.coeff 0)) < degree (divX p * X) :=
        calc
          degree (C (p.coeff 0)) ≤ 0 := degree_C_le
          _ < 1 := by decide
          _ = degree (X : R[X]) := degree_X.symm
          _ ≤ degree (divX p * X) := by
            rw [← zero_add (degree X), degree_mul' this]
            exact add_le_add
              (by rw [zero_le_degree_iff, Ne.def, divX_eq_zero_iff]
                  exact fun h0 => h (h0.symm ▸ degree_C_le))
                  le_rfl
      rw [degree_add_eq_left_of_degree_lt this]; exact degree_lt_degree_mul_X hXp0
  _ = degree p := congr_arg _ (divX_mul_X_add _)
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : degree p ≤ 0
h' : ↑C (coeff p 0) ≠ 0
⊢ degree (divX p) < degree (divX p * X + ↑C (coeff p 0))
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : degree p ≤ 0
⊢ degree (divX p) < degree (divX p * X + ↑C (coeff p 0))
have h' : C (p.coeff 0) ≠ 0 := by rwa [← eq_C_of_degree_le_zero h]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : degree p ≤ 0
h' : ↑C (coeff p 0) ≠ 0
⊢ ⊥ < degree (↑C (coeff (↑C (coeff p 0)) 0))
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : degree p ≤ 0
h' : ↑C (coeff p 0) ≠ 0
⊢ degree (divX p) < degree (divX p * X + ↑C (coeff p 0))
rw [eq_C_of_degree_le_zero h, divX_C, degree_zero, zero_mul, zero_add]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : degree p ≤ 0
h' : ↑C (coeff p 0) ≠ 0
⊢ ⊥ < degree (↑C (coeff (↑C (coeff p 0)) 0))
exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 <| by simpa using h'))
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : degree p ≤ 0
⊢ ↑C (coeff p 0) ≠ 0
rwa [← eq_C_of_degree_le_zero h]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : degree p ≤ 0
h' : ↑C (coeff p 0) ≠ 0
⊢ ¬↑C (coeff (↑C (coeff p 0)) 0) = 0
simpa using h'
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
⊢ degree (divX p) < degree (divX p * X + ↑C (coeff p 0))
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬degree p ≤ 0
⊢ degree (divX p) < degree (divX p * X + ↑C (coeff p 0))
have hXp0 : divX p ≠ 0 := by
  simpa [divX_eq_zero_iff, -not_le, degree_le_zero_iff] using h
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
this : leadingCoeff (divX p) * leadingCoeff X ≠ 0
⊢ degree (divX p) < degree (divX p * X + ↑C (coeff p 0))
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
⊢ degree (divX p) < degree (divX p * X + ↑C (coeff p 0))
have : leadingCoeff (divX p) * leadingCoeff X ≠ 0 := by simpa
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this✝¹ : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
this✝ : leadingCoeff (divX p) * leadingCoeff X ≠ 0
this : degree (↑C (coeff p 0)) < degree (divX p * X)
⊢ degree (divX p) < degree (divX p * X + ↑C (coeff p 0))
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
this : leadingCoeff (divX p) * leadingCoeff X ≠ 0
⊢ degree (divX p) < degree (divX p * X + ↑C (coeff p 0))
have : degree (C (p.coeff 0)) < degree (divX p * X) :=
  calc
    degree (C (p.coeff 0)) ≤ 0 := degree_C_le
    _ < 1 := by decide
    _ = degree (X : R[X]) := degree_X.symm
    _ ≤ degree (divX p * X) := by
      rw [← zero_add (degree X), degree_mul' this]
      exact add_le_add
        (by rw [zero_le_degree_iff, Ne.def, divX_eq_zero_iff]
            exact fun h0 => h (h0.symm ▸ degree_C_le))
            le_rfl
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this✝¹ : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
this✝ : leadingCoeff (divX p) * leadingCoeff X ≠ 0
this : degree (↑C (coeff p 0)) < degree (divX p * X)
⊢ degree (divX p) < degree (divX p * X)
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this✝¹ : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
this✝ : leadingCoeff (divX p) * leadingCoeff X ≠ 0
this : degree (↑C (coeff p 0)) < degree (divX p * X)
⊢ degree (divX p) < degree (divX p * X + ↑C (coeff p 0))
rw [degree_add_eq_left_of_degree_lt this]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this✝¹ : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
this✝ : leadingCoeff (divX p) * leadingCoeff X ≠ 0
this : degree (↑C (coeff p 0)) < degree (divX p * X)
⊢ degree (divX p) < degree (divX p * X)
exact degree_lt_degree_mul_X hXp0
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬degree p ≤ 0
⊢ divX p ≠ 0
simpa [divX_eq_zero_iff, -not_le, degree_le_zero_iff] using h
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
⊢ leadingCoeff (divX p) * leadingCoeff X ≠ 0
simpa
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
this : leadingCoeff (divX p) * leadingCoeff X ≠ 0
⊢ 0 < 1
decide
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
this : leadingCoeff (divX p) * leadingCoeff X ≠ 0
⊢ 0 + degree X ≤ degree (divX p) + degree X
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
this : leadingCoeff (divX p) * leadingCoeff X ≠ 0
⊢ degree X ≤ degree (divX p * X)
rw [← zero_add (degree X), degree_mul' this]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
this : leadingCoeff (divX p) * leadingCoeff X ≠ 0
⊢ 0 + degree X ≤ degree (divX p) + degree X
exact add_le_add
  (by rw [zero_le_degree_iff, Ne.def, divX_eq_zero_iff]
      exact fun h0 => h (h0.symm ▸ degree_C_le))
      le_rfl
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
this : leadingCoeff (divX p) * leadingCoeff X ≠ 0
⊢ ¬p = ↑C (coeff p 0)
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
this : leadingCoeff (divX p) * leadingCoeff X ≠ 0
⊢ 0 ≤ degree (divX p)
rw [zero_le_degree_iff, Ne.def, divX_eq_zero_iff]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p q : R[X]
hp0 : p ≠ 0
this✝ : Nontrivial R
h : ¬degree p ≤ 0
hXp0 : divX p ≠ 0
this : leadingCoeff (divX p) * leadingCoeff X ≠ 0
⊢ ¬p = ↑C (coeff p 0)
exact fun h0 => h (h0.symm ▸ degree_C_le)