English
Let p, q be polynomials over a semiring R. If p q ≠ 0, then the sum of their natTrailingDegrees is bounded above by the natTrailingDegree of their product: natTrailingDegree(p) + natTrailingDegree(q) ≤ natTrailingDegree(p q).
Русский
Пусть p, q — многочлены над полем R. Если p q ≠ 0, то сумма их natTrailingDegree не превосходит natTrailingDegree произведения: natTrailingDegree(p) + natTrailingDegree(q) ≤ natTrailingDegree(p q).
LaTeX
$$$ (p q) \neq 0 \Rightarrow \operatorname{natTrailingDegree}(p) + \operatorname{natTrailingDegree}(q) \le \operatorname{natTrailingDegree}(p q) $$$
Lean4
theorem le_natTrailingDegree_mul (h : p * q ≠ 0) :
p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).natTrailingDegree :=
by
have hp : p ≠ 0 := fun hp => h (by rw [hp, zero_mul])
have hq : q ≠ 0 := fun hq => h (by rw [hq, mul_zero])
rw [← WithTop.coe_le_coe, WithTop.coe_add, ← Nat.cast_withTop (natTrailingDegree p), ←
Nat.cast_withTop (natTrailingDegree q), ← Nat.cast_withTop (natTrailingDegree (p * q)), ←
trailingDegree_eq_natTrailingDegree hp, ← trailingDegree_eq_natTrailingDegree hq, ←
trailingDegree_eq_natTrailingDegree h]
exact le_trailingDegree_mul
