natDegree_eq_of_natDegree_add_lt_left

English

If natDegree(p+q) < natDegree(p), then natDegree(p) = natDegree(q).

Русский

Если natDegree(p+q) < natDegree(p), то natDegree(p) = natDegree(q).

LaTeX

$$$natDegree(p + q) < natDegree(p) \Rightarrow natDegree(p) = natDegree(q)$$$

Lean4

theorem natDegree_eq_of_natDegree_add_lt_left (p q : R[X]) (H : natDegree (p + q) < natDegree p) :
    natDegree p = natDegree q := by
  by_contra h
  cases Nat.lt_or_lt_of_ne h with
  | inl h => exact lt_asymm h (by rwa [natDegree_add_eq_right_of_natDegree_lt h] at H)
  | inr h =>
    rw [natDegree_add_eq_left_of_natDegree_lt h] at H
    exact LT.lt.false H

Похожие утверждения