{ n in ZZ : 2^n > n^2 }, an inequality with an exponential or a factorial over
the whole numbers, is searched over a window from the least member and its tails are
proved: the members are the points of the window where it holds, and the whole numbers
from the start of the final run where the quantifier decides it holds there -- by
induction, which is how Sullivan and Mackey do it (Ex 5.3.2: {0, 1} \/ ZZ /\ [5; +oo)).
Over ZZ the other tail is proved the same way, downwards. A tail the quantifier
leaves undecided leaves the set as written: a window is evidence about the window.
https://github.com/asc-community/AngouriMath/issues/1409