R : Type u
S : Type v
a b : R
n m : ℕ
inst✝¹ : Semiring R
p q✝ r : R[X]
inst✝ : Semiring S
q : S[X]
h : trailingDegree p = trailingDegree q
⊢ Option.getD (trailingDegree p) 0 = Option.getD (trailingDegree q) 0
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝¹ : Semiring R
p q✝ r : R[X]
inst✝ : Semiring S
q : S[X]
h : trailingDegree p = trailingDegree q
⊢ natTrailingDegree p = natTrailingDegree q
unfold natTrailingDegree
no goals
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝¹ : Semiring R
p q✝ r : R[X]
inst✝ : Semiring S
q : S[X]
h : trailingDegree p = trailingDegree q
⊢ Option.getD (trailingDegree p) 0 = Option.getD (trailingDegree q) 0
rw [h]