COQ is an interactive theorem prover that uses the calculus of inductive constructions, i.e. it relies heavily on inductive types. Using those, discrete structures like natural numbers, rational numbers, graphs, grammars, semantics etc. are very concisely represented.
However, since I grew to like the proof assistant, I was wondering whether there are libraries for uncountable structures, like real numbers, complex numbers, probability bounds and such. I am of course aware that one cannot define these structures inductively (at least not as far as I know), but they can be defined axiomatically, using for instance the axiomatic approach.
Is there any work that provides basic properties, or even probabilistic bounds like Chernoff bound or union bound as a library?