natDegree_sub_eq_right_of_natDegree_lt

English

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

Русский

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

LaTeX

$$$\operatorname{natDegree}(p - q) = \operatorname{natDegree}(q) \quad\text{if } \operatorname{natDegree}(p) < \operatorname{natDegree}(q)$$$

Lean4

theorem natDegree_sub_eq_right_of_natDegree_lt (h : natDegree p < natDegree q) : natDegree (p - q) = natDegree q :=
  natDegree_eq_of_degree_eq (degree_sub_eq_right_of_degree_lt (degree_lt_degree h))

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