[kgilpin]

As far as I know, addition is something you define (an axiom) in order to construct the real (or other) numbers.

https://sites.math.washington.edu/~hart/m524/realprop.pdf