Coinduction in mathematical analysis?
The signed digit representation of Real Numbers seems like an efficient approach for:


Defining the arithmetic operations and proving their algebraic properties. This was done already in a Master's thesis by Michael Herrmann.
Proving Cantor's theorem on the uncountability of the real numbers.
Developing the notions of continuous and uniformly continuous functions.
Proving the Extreme Value Theorem in the form that every function on $[0,1]$ has a finite supremum.
Developing the Riemann integral.


This has the nice property of being constructive.

As demonstrated by Michael Hermann, the operations listed above can be defined using colagebraic coinduction and then reasoned about using set-theoretic coinduction.

This also suggests the possibility of proving analogues of the above in $p$-adic analysis. Here, a purely coalgebraic approach might actually work.

It's possible that vast swathes of General Topology (over separable spaces) can be developed using coinduction over $\mathbb N^\mathbb N$. Here, continuous functions would be defined by corecursion over $\mathbb N ^ \mathbb N$ and then reasoned about using set-theoretic coinduction. This appears to be the approach taken in Frank'a Waaldijk's Natural Topology (I'm not sure if it uses coinduction though).

The caveat of all the above is that I've never seen a full development of the above. But the possibility certainly exists if anyone has the time or motivation.