We present two methods for defining corecursive functions that go beyond what the dedicated mechanisms of the Coq proof assistant for defining such functions are able to accept. The first method uses those same dedicated mechanisms, but in a manner that is substantially different from the standard one available in Coq. It can be used to define corecursive functions as long as the functions’ codomains are coinductive types not mutually dependent with inductive types. The second method is not subject to these restrictions, because it does not use Coq’s dedicated mechanisms for corecursion but redefines them. Both methods amount to defining corecursive functions as limits of sequences of approximations, and both require a property of productiveness that, intuitively, means that for each input, an arbitrarily close approximation of the limit’s corresponding output is eventually obtained. The methods are implemented in Coq and are illustrated with examples of corecursive functions that go beyond Coq’s builtin capabilities. This gain in expressiveness is obtained by using a combination of axioms from Coq’s standard library that enable reasoning in standard (i.e., not necessarily constructive) mathematics.