case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : a = 0
⊢ degree (↑C a) ≤ 0

case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : ¬a = 0
⊢ degree (↑C a) ≤ 0
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ degree (↑C a) ≤ 0
by_cases h : a = 0
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : a = 0
⊢ degree 0 ≤ 0
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : a = 0
⊢ degree (↑C a) ≤ 0
rw [h, C_0]
no goals
case pos
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : a = 0
⊢ degree 0 ≤ 0
exact bot_le
no goals
case neg
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : ¬a = 0
⊢ degree (↑C a) ≤ 0
rw [degree_C h]