  We give a quantifier elimination procedures for the extension of Presburger
arithmetic with a unary threshold counting quantifier $\exists^{\ge c} y$ that
determines whether the number of different $y$ satisfying some formula is at
least $c \in \mathbb N$, where $c$ is given in binary. Using a standard
quantifier elimination procedure for Presburger arithmetic, the resulting
theory is easily seen to be decidable in 4ExpTime. Our main contribution is to
develop a novel quantifier-elimination procedure for a more general counting
quantifier that decides this theory in 3ExpTime, meaning that it is no harder
to decide than standard Presburger arithmetic. As a side result, we obtain an
improved quantifier elimination procedure for Presburger arithmetic with
counting quantifiers as studied by Schweikardt [ACM Trans. Comput. Log., 6(3),
pp. 634-671, 2005], and a 3ExpTime quantifier-elimination procedure for
Presburger arithmetic extended with a generalised modulo counting quantifier.
