English
Under the same assumptions as degree_divByMonic_lt, the degree of the quotient is strictly smaller than the degree of p.
Русский
При тех же предпосылках, что и degree_divByMonic_lt, deg(p /ₘ q) < deg p.
LaTeX
$$$ \deg(p /_{m} q) < \deg p \quad \text{при тех же условиях} $$$
Lean4
theorem degree_divByMonic_le (p q : R[X]) : degree (p /ₘ q) ≤ degree p :=
letI := Classical.decEq R
if hp0 : p = 0 then by simp only [hp0, zero_divByMonic, le_refl]
else
if hq : Monic q then
if h : degree q ≤ degree p then by
haveI := Nontrivial.of_polynomial_ne hp0
rw [← degree_add_divByMonic hq h, degree_eq_natDegree hq.ne_zero,
degree_eq_natDegree (mt (divByMonic_eq_zero_iff hq).1 (not_lt.2 h))]
exact WithBot.coe_le_coe.2 (Nat.le_add_left _ _)
else by
unfold divByMonic divModByMonicAux
simp [dif_pos hq, h, degree_zero, bot_le]
else (divByMonic_eq_of_not_monic p hq).symm ▸ bot_le
