  The purpose of this paper is to develop and study recursive proofs of
coinductive predicates. Such recursive proofs allow one to discover proof goals
in the construction of a proof of a coinductive predicate, while still allowing
the use of up-to techniques. This approach lifts the burden to guess
invariants, like bisimulation relations, beforehand. Rather, they allow one to
start with the sought-after proof goal and develop the proof from there until a
point is reached, at which the proof can be closed through a recursion step.
Proofs given in this way are both easier to construct and to understand,
similarly to proofs given in cyclic proof systems or by appealing parameterised
coinduction.
  In this paper, we develop a framework for recursive proofs of coinductive
predicates that are given through fibrational predicate liftings. This
framework is built on the so-called later modality, which has made its
appearance in type theoretic settings before. In particular, we show the
soundness and completeness of recursive proofs, we prove that compatible up-to
techniques can be used as inference rules in recursive proofs, and provide some
illustrating examples.
