Differences, Quotients and Absolute Values of Real Numbers, Read in the Type Real

In the setting of The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness, let $x$ and $y$ be real numbers, read as elements of the type $\mathrm{Real}$ of The Real Numbers as a Type (i) where a type is required, with $0$, $+$, $\cdot$, $-$ and $\le$ those of $\mathrm{Real}$ as in The Real Numbers as a Type (ii) and The Real Numbers as a Type (iii), and $<$ the strict relation of $\le$.

(i) The difference $x-y$ lies in $\mathbb{R}$ and equals $x+(-y)$, the difference of $x$ and $y$ in $\mathrm{Real}$.

(ii) If $y\neq0$, then the quotient $x/y$ lies in $\mathbb{R}$, so it is an element of $\mathrm{Real}$, and equals $x\cdot y^{-1}$, where $y^{-1}$ is the reciprocal of $y$, and $(x/y)\cdot y=x$.

(iii) The absolute value $|x|$ lies in $\mathbb{R}$; $|x|=x$ if $0\le x$, and $|x|=-x$ if $x<0$; $0\le|x|$; and $|x-y|=|y-x|$.