Int.pairwise_one_le_dist

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

This theorem states that for every pair of distinct integer numbers `m` and `n`, the distance between `m` and `n` (denoted as `dist m n`) is always greater than or equal to 1. In other words, the pairwise distance between any two different integers is always at least 1.

More concisely: For all integers m and n with m ≠ n, dist(m, n) ≥ 1.