Mathlib.Data.Nat.Dist
source
This file defines a simple distance function on naturals from truncated subtraction.
Distance (absolute value of difference) between natural numbers.