Coq implementation of O(n log n) algorithm for closest pair of points in a plane