English
Another instance of the same degree-drop property for a monic divisor q with p ≠ 0.
Русский
Еще одно приложение свойства понижать степень при моническом делителе.
LaTeX
$$$ \deg(p /_{m} q) < \deg p \quad (\operatorname{Monic}(q),\; p \neq 0) $$$
Lean4
theorem degree_divByMonic_lt (p : R[X]) {q : R[X]} (hq : Monic q) (hp0 : p ≠ 0) (h0q : 0 < degree q) :
degree (p /ₘ q) < degree p :=
if hpq : degree p < degree q then by
haveI := Nontrivial.of_polynomial_ne hp0
rw [(divByMonic_eq_zero_iff hq).2 hpq, degree_eq_natDegree hp0]
exact WithBot.bot_lt_coe _
else by
haveI := Nontrivial.of_polynomial_ne hp0
rw [← degree_add_divByMonic hq (not_lt.1 hpq), degree_eq_natDegree hq.ne_zero,
degree_eq_natDegree (mt (divByMonic_eq_zero_iff hq).1 hpq)]
exact Nat.cast_lt.2 (Nat.lt_add_of_pos_left (Nat.cast_lt.1 <| by simpa [degree_eq_natDegree hq.ne_zero] using h0q))
