Nat.pairwise_one_le_dist

theorem Nat.pairwise_one_le_dist : Pairwise fun m n => 1 ≤ dist m n

This theorem states that the pairwise distance between any two distinct natural numbers is always greater than or equal to 1. In other words, for every pair of different natural numbers `m` and `n`, the absolute difference between `m` and `n` (denoted as `dist m n`) is at least 1. This statement aligns with the intuitive notion of distance in the set of natural numbers.

More concisely: For all natural numbers m and n with m ≠ n, |m - n| ≥ 1.