English
If y ≠ 0 and x+y ≠ 0, then intDegree(x+y) ≤ max(intDegree(x), intDegree(y)).
Русский
Если y ≠ 0 и x+y ≠ 0, то intDegree(x+y) ≤ max(intDegree(x), intDegree(y)).
LaTeX
$$$y \\neq 0 \\;\\land\\; x+y \\neq 0 \\Rightarrow \\operatorname{intDegree}(x+y) \\le \\max\\left(\\operatorname{intDegree}(x), \\operatorname{intDegree}(y)\\right)$$$
Lean4
theorem intDegree_add_le {x y : RatFunc K} (hy : y ≠ 0) (hxy : x + y ≠ 0) :
intDegree (x + y) ≤ max (intDegree x) (intDegree y) :=
by
by_cases hx : x = 0
· simp [hx]
rw [intDegree_add hxy, ← natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree hx y.denom_ne_zero,
mul_comm y.denom, ← natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree hy x.denom_ne_zero,
le_max_iff, sub_le_sub_iff_right, Int.ofNat_le, sub_le_sub_iff_right, Int.ofNat_le, ← le_max_iff, mul_comm y.num]
exact natDegree_add_le _ _
