Start formalizing limits

[fzaiser]

This is needed to properly define infinite sums (used in the definition of measures) and the exponential function.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[jtristan]

Split into multiple files by theme. Perhaps one for nl arithmetic results, one for abs, one for sequences, one for limit. Should we abstract a bit? (say, metric spaces). We should think about whether we expect such generalization to be useful eventually

[fzaiser]

@jtristan I split it into three files: one for facts about the reals, one for sequences and one for limits. I'd rather not go into too much generality regarding metric spaces yet, as I don't see a need for them any time soon.