le_natCast_sub — Mathlib

English

For naturals m,n, the integer subtraction m − n is always less than or equal to the natural subtraction cast into integers.

Русский

Для натуральных чисел m,n целочисленное вычитание m − n не превосходит перевод натуральной разности в целые числа.

LaTeX

$$$\forall m,n \in \mathbb{N},\ (m-n \in \mathbb{Z}) \le (m-n)\_\mathbb{N}$$$$

Lean4

theorem le_natCast_sub (m n : ℕ) : (m - n : ℤ) ≤ ↑(m - n : ℕ) := by cutsat

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