In EWD687, Scholten and I used without proof the (rather obvious)
Theorem. In a directed, finite graph, such that
a) any node with an incoming edge has outgoing edges, and
b) no node has more than one incoming edge,
the edges form only directed cyclic paths.
I gave myself the task to find a proof as nice as the theorem is obvious. The following one I really like.
Let for each node IN be the number of its incoming edges and OUT the number of its outgoing edges. Then a) states that for each node we have