natAbs_coe_sub_coe_le_of_le — Mathlib

English

If a,b,n are naturals with a ≤ n and b ≤ n, then the absolute value of (a−b) considered as an integer is at most n.

Русский

Если a,b,n ∈ ℕ и a ≤ n, b ≤ n, то |a−b| как целое не превосходит n.

LaTeX

$$$\forall a,b,n \in \mathbb{N},\ a \le n \rightarrow b \le n \rightarrow |(a-b) |_{\mathbb{Z}} \le n$$$

Lean4

/-- A specialization of `abs_sub_le_of_nonneg_of_le` for working with the signed subtraction
  of natural numbers. -/
theorem natAbs_coe_sub_coe_le_of_le {a b n : ℕ} (a_le_n : a ≤ n) (b_le_n : b ≤ n) : natAbs (a - b : ℤ) ≤ n :=
  by
  rw [← Nat.cast_le (α := ℤ), natCast_natAbs]
  exact abs_sub_le_of_nonneg_of_le (natCast_nonneg a) (ofNat_le.mpr a_le_n) (natCast_nonneg b) (ofNat_le.mpr b_le_n)

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