English
If q is monic and deg q ≤ deg p with p ≠ 0, then the leading-term subtraction p − (leadingCoeff p) X^{natDegree p − natDegree q} · q strictly reduces the degree of p.
Русский
Если q монический и deg q ≤ deg p при p ≠ 0, то вычитание p − (ведущий коэффициент p) X^{natDegree(p) − natDegree(q)} · q уменьшает степень p.
LaTeX
$$$ (\deg q \le \deg p) \wedge (p \neq 0) \wedge \operatorname{Monic}(q) \Rightarrow \\ \deg\left(p - q \cdot \bigl(\mathrm{leadingCoeff}(p) \cdot X^{\operatorname{natDegree}(p) - \operatorname{natDegree}(q)}\bigr)\right) < \deg p $$$
Lean4
theorem div_wf_lemma (h : degree q ≤ degree p ∧ p ≠ 0) (hq : Monic q) :
degree (p - q * (C (leadingCoeff p) * X ^ (natDegree p - natDegree q))) < degree p :=
have hp : leadingCoeff p ≠ 0 := mt leadingCoeff_eq_zero.1 h.2
have hq0 : q ≠ 0 := hq.ne_zero_of_polynomial_ne h.2
have hlt : natDegree q ≤ natDegree p :=
(Nat.cast_le (α := WithBot ℕ)).1 (by rw [← degree_eq_natDegree h.2, ← degree_eq_natDegree hq0]; exact h.1)
degree_sub_lt
(by
rw [hq.degree_mul_comm, hq.degree_mul, degree_C_mul_X_pow _ hp, degree_eq_natDegree h.2, degree_eq_natDegree hq0,
← Nat.cast_add, tsub_add_cancel_of_le hlt])
h.2 (by rw [leadingCoeff_monic_mul hq, leadingCoeff_mul_X_pow, leadingCoeff_C])
