About 0.999... = 1 I've just happened to read this question on MO (that of course has been closed) and some of the answers to a similar question on MSE. 
I know almost nothing of nonstandard analysis and was asking myself if something like the sentence « $1- 0.999 \dots$ is a nonzero positive infinitesimal» could be easily expressed and proved in nonstandard analysis.
First of all, what is 0.999... ? If we take the usual definition as a series or as a limit of a sequence of rationals, then it will still be a real number and equal to $1$ (I guess by "transfer principle", but please correct me if I'm wrong).
Instead, let's define
$$0.9_N:=\sum_{i=1}^N 9\cdot 10^{-i} $$
where $N\in{}^*\mathbb{N}\setminus\mathbb{N}$ is an infinite nonstandard natural number. This $0.9_N$ is a legitimate element of ${}^*\mathbb{R}$, expressed as $0.$ followed by an infinite number of "$9$" digits.
What can be said about $\epsilon_N:=1-0.9_N$ ? Is there an elementary proof that $\epsilon_N$ is a positive infinitesimal of ${}^*\mathbb{R}$ ? (by "elementary" I mean just order and field axioms and the intuitive facts about infinitesimals, like that for $x$ infinite $1/x$ is infinitesimal etc.; no nonprincipal ultrafilters & C).
 A: $$1-\sum_{k=1}^N9\cdot10^{-k}=\sum_{k\ge N+1}9\cdot 10^{-k}=9\sum_{k\ge N+1}10^{-k}=\frac{9\cdot 10^{-(N+1)}}{1-10^{-1}}=10^{-N}=\frac1{10^N}\;,$$
which is surely intuitively a positive infinitesimal.
Added: There is a nice elementary axiomatization of the hyperreals in Jerry Keisler’s Elementary Calculus: An infinitesimal approach, which is freely available here; it is intended for students in a first calculus course and neatly avoids the transfer principle as such. His Foundations of infinitesimal calculus contains a slightly more sophisticated version, since it’s intended for instructors using the undergraduate text. It’s freely available here, and its version of the axiomatic development can also be found in Section $15$ of this PDF. What he calls the Function Axiom (Axiom $C$ in the PDF) justifies the standard calculation:

For each real function $f$ of $n$ variables there is a corresponding hyperreal function ${}^*f$ of $n$ variables, called the natural extension of $f$.

The function in question here is the function that takes $n$ to $\sum_{k=1}^n9\cdot10^{-k}$.
A slightly different version of this approach is found in Keith Stroyan’s notes here, especially Section $2.3$.
A: In addition to the fine answers given earlier, I would like to mention also the somewhat unsung hero, A. H. Lightstone, and his extended decimal notation in which your infinitesimal $\epsilon_N$ can be written as $0.000\ldots;\ldots 0001$, where the first nonzero digit occurs precisely at infinite rank $N$.  The notation is explained in his article in the American Mathematical Monthly (see especially page 246).
A: We can use the geometric series formula:
$$0.9_N = \sum_{i=1}^N 9 \cdot 10^{-i} = 9 \cdot 10^{-1} \cdot \frac{1 - 10^{-N}}{1 - 10^{-1}}  = (1 - 10^{-N})$$
Since $N$ is infinite, $\epsilon_N = 10^{-N} = 1 / 10^N$ is infinitesimal.
