Unit-distance count for a finite planar point set

Read-back. The declaration introduces a function named unitDist which takes one explicit argument $P$ — a finite set (a Finset, i.e. a finite, duplicate-free collection) of points of the space $\mathrm{EuclideanSpace}\ \mathbb{R}\ (\mathrm{Fin}\ 2)$, that is, the set of functions from the two-element index type $\{0,1\}$ to $\mathbb{R}$ equipped with the $\ell^2$ (Euclidean) norm, so that the distance used is $\operatorname{dist}(p,q)=\sqrt{(p_0-q_0)^2+(p_1-q_1)^2}$ — and returns a natural number; the function is declared noncomputable and the file opens Classical, so the decidability of the filtering predicate below is supplied by classical choice rather than by an algorithm, which affects only computability and not the mathematical value. The returned number is computed as follows: one forms $P.\mathrm{offDiag}$, the finite set of ordered pairs $(p,q)$ with $p\in P$, $q\in P$ and $p\neq q$ (the product $P\times P$ with the diagonal removed; note that both $(p,q)$ and $(q,p)$ occur); one keeps exactly those pairs whose first and second components are at Euclidean distance exactly $1$, i.e. $\operatorname{dist}(p,q)=1$ as an equality of real numbers (not an approximation and not an inequality); one takes the cardinality of that filtered finite set, a natural number; and finally one divides that cardinality by $2$ using natural-number division, which truncates toward zero, so the value is

No hypotheses whatsoever are imposed on $P$: it may be empty or a singleton, in which case the off-diagonal is empty and the value is $0$; it may contain no pair at distance $1$, again giving $0$; and because the count ranges over ordered pairs while the divisor is $2$, the definition returns half of the number of ordered unit-distance pairs, with any odd remainder silently discarded by the floor of natural division rather than flagged as an error. Distance is taken between the two components of each pair only, with no further geometric condition (no collinearity, general position, or distinctness beyond $p\neq q$), and the ambient space is fixed to be two-dimensional real Euclidean space; the definition is a plain function with no output specification, no quantifiers other than the single argument $P$, and no typeclass hypotheses beyond those already fixed by the type and by Finset's requirement that $P$ be finite.