Coinduction is an important concept in functional programming. To formally prove properties of corecursive functions one can try to
define them in a proof assistant such as Coq. But there are
limitations on the  functions that can be defined in this manner: corecursive calls must occur directly under a call to a constructor, without any  calls to other recursive functions in between. In this paper we show how certain extensions of partially ordered sets can be organized as Complete Partial Orders endowed with the same extensions. This makes it possible to define total corecursive functions as unique solutions of their fixpoint equations, provided that the functionals involved in the equation satisfy a certain productiveness requirement. The result is a generic approach for defining total corecursive functions in Coq that escape the tool's builtin limitations.