A Universe of Sorts

If we can solve for number of elements <= k, say given by leq(k) where k is an integer, then we can also solve for number of elements = k, given by eq(k) := leq(k) - leq(k - 1).
While simple, this is hugely benificial in many situations because <=k can be implement as some kind of prefix sum data structure plus binary search, which is much less error prone to hack up than exact equality.

§ CP Trick: Writing Exact Counting as Counting Less Than