This paper describes a functor-generic
derivation in Coq of subsidiary recursion. With
this recursion scheme, inner recursions may be
initiated within outer ones, in such a way that
outer recursive calls may be made on results
from inner ones. The derivation utilizes a novel
(necessarily weakened) form of
positive-recursive types in Coq, dubbed
retractive-positive recursive types. A
corresponding form of induction is also
supported. The method is demonstrated through
several examples.