R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
P : R[X] → Prop
p : R[X]
h0 : 0 < degree p
hC : ∀ {a : R}, a ≠ 0 → P (↑C a * X)
hX : ∀ {p : R[X]}, 0 < degree p → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < degree p → P p → P (p + ↑C a)
h : 0 < ⊥
⊢ 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]
P : R[X] → Prop
p : R[X]
h0 : 0 < degree p
hC : ∀ {a : R}, a ≠ 0 → P (↑C a * X)
hX : ∀ {p : R[X]}, 0 < degree p → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < degree p → P p → P (p + ↑C a)
h : 0 < degree 0
⊢ P 0
rw [degree_zero] at 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]
P : R[X] → Prop
p : R[X]
h0 : 0 < degree p
hC : ∀ {a : R}, a ≠ 0 → P (↑C a * X)
hX : ∀ {p : R[X]}, 0 < degree p → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < degree p → P p → P (p + ↑C a)
h : 0 < ⊥
⊢ P 0
exact absurd h (by decide)
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]
P : R[X] → Prop
p : R[X]
h0 : 0 < degree p
hC : ∀ {a : R}, a ≠ 0 → P (↑C a * X)
hX : ∀ {p : R[X]}, 0 < degree p → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < degree p → P p → P (p + ↑C a)
h : 0 < ⊥
⊢ ¬0 < ⊥
decide
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]
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < degree p✝
hC : ∀ {a : R}, a ≠ 0 → P (↑C a * X)
hX : ∀ {p : R[X]}, 0 < degree p → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < degree p → P p → P (p + ↑C a)
p : R[X]
a : R
x✝¹ : coeff p 0 = 0
x✝ : a ≠ 0
ih : 0 < degree p → P p
h0 : 0 < degree (p + ↑C a)
h : 0 ≥ degree p
⊢ 0 < degree (↑C (?m.236563 p a x✝¹ x✝ ih h0 h))
rwa [eq_C_of_degree_le_zero h, ← C_add] at h0
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝¹ q : R[X]
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < degree p✝
hC : ∀ {a : R}, a ≠ 0 → P (↑C a * X)
hX : ∀ {p : R[X]}, 0 < degree p → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < degree p → P p → P (p + ↑C a)
p : R[X]
x✝ : p ≠ 0
ih : 0 < degree p → P p
h0' : 0 < degree (↑C (coeff p 0) * X)
h0 : ¬0 < degree p
⊢ P (↑C (coeff p 0) * X)
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝¹ q : R[X]
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < degree p✝
hC : ∀ {a : R}, a ≠ 0 → P (↑C a * X)
hX : ∀ {p : R[X]}, 0 < degree p → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < degree p → P p → P (p + ↑C a)
p : R[X]
x✝ : p ≠ 0
ih : 0 < degree p → P p
h0' : 0 < degree (p * X)
h0 : ¬0 < degree p
⊢ P (p * X)
rw [eq_C_of_degree_le_zero (le_of_not_gt h0)] at h0' ⊢
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]
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < degree p✝
hC : ∀ {a : R}, a ≠ 0 → P (↑C a * X)
hX : ∀ {p : R[X]}, 0 < degree p → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < degree p → P p → P (p + ↑C a)
p : R[X]
x✝ : p ≠ 0
ih : 0 < degree p → P p
h0' : 0 < degree (↑C (coeff p 0) * X)
h0 : ¬0 < degree p
⊢ P (↑C (coeff p 0) * X)
exact hC fun h : coeff p 0 = 0 => by simp [h, Nat.not_lt_zero] at h0'
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]
P : R[X] → Prop
p✝ : R[X]
h0✝ : 0 < degree p✝
hC : ∀ {a : R}, a ≠ 0 → P (↑C a * X)
hX : ∀ {p : R[X]}, 0 < degree p → P p → P (p * X)
hadd : ∀ {p : R[X]} {a : R}, 0 < degree p → P p → P (p + ↑C a)
p : R[X]
x✝ : p ≠ 0
ih : 0 < degree p → P p
h0' : 0 < degree (↑C (coeff p 0) * X)
h0 : ¬0 < degree p
h : coeff p 0 = 0
⊢ False
simp [h, Nat.not_lt_zero] at h0'