English
If deg p = deg q, p ≠ 0, and leadingCoeff p = leadingCoeff q, then degree(p - q) < degree p.
Русский
Если deg p = deg q, p ≠ 0, и leadingCoeff p = leadingCoeff q, то degree(p - q) < degree p.
LaTeX
$$degree(p - q) < degree(p)$$
Lean4
theorem degree_sub_lt (hd : degree p = degree q) (hp0 : p ≠ 0) (hlc : leadingCoeff p = leadingCoeff q) :
degree (p - q) < degree p :=
have hp : monomial (natDegree p) (leadingCoeff p) + p.erase (natDegree p) = p := monomial_add_erase _ _
have hq : monomial (natDegree q) (leadingCoeff q) + q.erase (natDegree q) = q := monomial_add_erase _ _
have hd' : natDegree p = natDegree q := by unfold natDegree; rw [hd]
have hq0 : q ≠ 0 := mt degree_eq_bot.2 (hd ▸ mt degree_eq_bot.1 hp0)
calc
degree (p - q) = degree (erase (natDegree q) p + -erase (natDegree q) q) := by
conv =>
lhs
rw [← hp, ← hq, hlc, hd', add_sub_add_left_eq_sub, sub_eq_add_neg]
_ ≤ max (degree (erase (natDegree q) p)) (degree (erase (natDegree q) q)) :=
(degree_neg (erase (natDegree q) q) ▸ degree_add_le _ _)
_ < degree p := max_lt_iff.2 ⟨hd' ▸ degree_erase_lt hp0, hd.symm ▸ degree_erase_lt hq0⟩
