Notation in the Reals Library

I am currently reading through the Reals documentation.
In the file Raxioms, the third axiom given is :
Axiom Rplus_opp_r : forall r:R, r + - r = 0.
Hint Resolve Rplus_opp_r: real.
I would like to understand how the notation 0 has been introduced, as I can’t find it in explicitely anywhere. Do you have any clue ?

Thanks !

I might be wrong, but a quick search suggests that it’s defined in It’s basically IZR Z0.

Ok, thank you ! I haven’t encountered CaML files in Coq and don’t know how it works yet… I guess I’ll get back to that later.