R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
p q✝ r : R[X]
inst✝ : Semiring S
q : S[X]
h : degree p = degree q
⊢ WithBot.unbot' 0 (degree p) = WithBot.unbot' 0 (degree q)
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
p q✝ r : R[X]
inst✝ : Semiring S
q : S[X]
h : degree p = degree q
⊢ natDegree p = natDegree q
unfold natDegree
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝¹ : Semiring R
p q✝ r : R[X]
inst✝ : Semiring S
q : S[X]
h : degree p = degree q
⊢ WithBot.unbot' 0 (degree p) = WithBot.unbot' 0 (degree q)
rw [h]