natAbs_coe_sub_coe_lt_of_lt — 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 strictly less than n.

Русский

Если a,b < n, то |a−b|_ℤ < n.

LaTeX

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

Lean4

/-- A specialization of `abs_sub_lt_of_nonneg_of_lt` for working with the signed subtraction
  of natural numbers. -/
theorem natAbs_coe_sub_coe_lt_of_lt {a b n : ℕ} (a_lt_n : a < n) (b_lt_n : b < n) : natAbs (a - b : ℤ) < n :=
  by
  rw [← Nat.cast_lt (α := ℤ), natCast_natAbs]
  exact abs_sub_lt_of_nonneg_of_lt (natCast_nonneg a) (ofNat_lt.mpr a_lt_n) (natCast_nonneg b) (ofNat_lt.mpr b_lt_n)

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