The Reciprocal on the Type of Real Numbers

In the setting of The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness, with $\mathrm{Real}$ the type of The Real Numbers as a Type (i) and its operations and numerals as in The Real Numbers as a Type (ii) and The Real Numbers as a Type (iii): (i) for $x\ne0$ in $\mathrm{Real}$, the reciprocal $x^{-1}$ is the element of $\mathrm{Real}$ whose set (as in The Real Numbers as a Type (i)) is the reciprocal of $x$ in $\mathbb{R}$; this reciprocal lies in $\mathbb{R}$ and satisfies $x\cdot x^{-1}=1$ (Negatives, Reciprocals and the Strict Order in an Ordered Field, as Values (ii)). In Lean the reciprocal is $\mathtt{recipR}$.