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 ?