The Real Numbers as a Type

In the setting of The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness, where $\mathbb{R}$ is an ordered field by The Real Numbers Form an Ordered Field in Which Every Nonempty Set Bounded Above Has a Supremum (i): (i) $\mathrm{Real}$ is the type whose elements are the real numbers: an element of $\mathrm{Real}$ is a set $x\in\mathbb{R}$, carried with the fact that it lies in $\mathbb{R}$, and two elements are equal when their sets are (the one place where a real number is handled as a set, as a type requires). (ii) The elements $0$ and $1$, the operations $x+y$ and $x\cdot y$ and the order $x\le y$ of $\mathrm{Real}$ are those of $\mathbb{R}$ (The Real Numbers (iii), The Real Numbers (iv)); $-x$ is the negative, which lies in $\mathbb{R}$ by Negatives, Reciprocals and the Strict Order in an Ordered Field, as Values (i), and $x-y$ the difference $x+(-y)$; $x<y$ is the strict relation of $\le$. Reciprocals and quotients are not operations of $\mathrm{Real}$; they are taken in $\mathbb{R}$. (iii) Numerals and powers are read recursively: the natural number $0$ is $0$, $1$ is $1$ and $n+2$ is $(n+1)+1$; an integer $i\ge0$ is read as the natural number $i$, and $-(n+1)$ as the negative of $n+1$; $x^{0}=1$ and $x^{n+1}=x^{n}\cdot x$; and $n\cdot x$ and $i\cdot x$, for a natural number $n$ and an integer $i$, are the products of their readings with $x$. Since an element of $\mathrm{Real}$ is determined by its set and $\mathbb{R}$ is an ordered field, the laws of $\mathbb{R}$ hold for these operations and this order: (iv) the laws of a commutative ring hold for $+$, $\cdot$, $0$ and $1$ on $\mathrm{Real}$, among them $0\cdot x=0$, $-(-x)=x$ and $(-x)\cdot y=-(x\cdot y)$ (Rules of Arithmetic and Order in an Ordered Field (i), Rules of Arithmetic and Order in an Ordered Field (ii)) and $x+(-x)=0$ (Negatives, Reciprocals and the Strict Order in an Ordered Field, as Values (i)); (v) $\le$ on $\mathrm{Real}$ is reflexive, antisymmetric, transitive and total, as $\le$ is a total order on $\mathbb{R}$, and $x<y$ holds exactly when $x\le y$ and not $y\le x$ (Negatives, Reciprocals and the Strict Order in an Ordered Field, as Values (iii)); (vi) the laws of an ordered ring hold, in the forms $x\le y$ if and only if $x+z\le y+z$ (Rules of Order in an Ordered Ring: Differences, Sums, Negatives, Products and Squares (ii)), $0<1$ (Rules of Arithmetic and Order in an Ordered Field (vii)), and, if $x<y$ and $0<z$, then $x\cdot z<y\cdot z$ (Rules of Arithmetic and Order in an Ordered Field (vi)) and hence, by commutativity, $z\cdot x<z\cdot y$. In Lean these clauses are the classes $\mathtt{Lean.Grind.CommRing}$; $\mathtt{Std.IsLinearOrder}$ and $\mathtt{Std.LawfulOrderLT}$; and $\mathtt{Lean.Grind.OrderedAdd}$ and $\mathtt{Lean.Grind.OrderedRing}$.