no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.557539
h : leadingCoeff p + leadingCoeff q ≠ 0
hlt : degree p < degree q
⊢ max (degree p) (degree q) ≤ degree (p + q)
rw [degree_add_eq_right_of_degree_lt hlt, max_eq_right_of_lt hlt]
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.557539
h : leadingCoeff p + leadingCoeff q ≠ 0
HEq : degree p = degree q
hlt : degree q > degree (p + q)
⊢ leadingCoeff p + leadingCoeff q = 0
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.557539
h : leadingCoeff p + leadingCoeff q ≠ 0
HEq : degree p = degree q
hlt : max (degree p) (degree q) > degree (p + q)
⊢ leadingCoeff p + leadingCoeff q = 0
rw [HEq, max_self] at hlt
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.557539
h : leadingCoeff p + leadingCoeff q ≠ 0
HEq : degree p = degree q
hlt : degree q > degree (p + q)
⊢ coeff (p + q) (natDegree q) = 0
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.557539
h : leadingCoeff p + leadingCoeff q ≠ 0
HEq : degree p = degree q
hlt : degree q > degree (p + q)
⊢ leadingCoeff p + leadingCoeff q = 0
rw [leadingCoeff, leadingCoeff, natDegree_eq_of_degree_eq HEq, ← coeff_add]
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.557539
h : leadingCoeff p + leadingCoeff q ≠ 0
HEq : degree p = degree q
hlt : degree q > degree (p + q)
⊢ coeff (p + q) (natDegree q) = 0
exact coeff_natDegree_eq_zero_of_degree_lt hlt
no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.557539
h : leadingCoeff p + leadingCoeff q ≠ 0
hlt : degree q < degree p
⊢ max (degree p) (degree q) ≤ degree (p + q)
rw [degree_add_eq_left_of_degree_lt hlt, max_eq_left_of_lt hlt]