As you probably know, between choice and foundation, any use of coinductive arguments in ZFC can be eliminated. So you often have cases where coinduction could have been used, but more inductive methods  are used instead. So you have to squint a bit to see them.

Aside from CS and modal logic, the place where coinductive arguments show up most commonly is in game theory, in the study of Nash equilibria of infinite games. The reason they show up here is that it's natural to think of a game in terms of a stream or infinite tree of player moves and opponent responses. If you think about it, this is very similar to the situation in process algebra, where you think of the interaction between a process and its environment. 

This actually tells you where to look to find coinduction in the central areas of mathematics. In particular, Nash equilibrium can be understood as an application of Brouwer's fixed point theorem, which tells you that any time you see a compactness or completeness requirement, that's something that could be explained coinductively. 

Basically, the intuition is that taking an infinite number of steps always takes you to a limit, and "taking an infinite number of steps" is essentially a function $\mathbb{N} \to \mathrm{blah}$, which is isomorphic to a *stream* of $\mathrm{blah}$s. This fact is of considerable importance in implementations of computable real arithmetic, because Cauchy sequences are streams, too, and it is natural to write corecursive programs to work with them.