We implement in Gallina a hierarchy of functions that calculate the upper inverses to the hyperoperation/Ackermann hierarchy. Our functions run in $\Theta(b)$ for inputs expressed in unary, and in $O(b^2)$ for inputs expressed in binary (where $b$ = bitlength). We use our inverses to define linear-time functions—$\Theta(b)$ for both unary-represented and binary-represented inputs—that compute the upper inverse of the diagonal Ackermann function $\mathcal{A}(n)$. We show that these functions are consistent with the usual definition of the inverse Ackermann function $\alpha(n)$.