\chapter{Explicit Reals}
\section{explicit\_Reals}\label{fgihahmgjgdgjgehpfcffgbgmgdh}Let $ R : {\iota}$ be given.
Let $ zero, one : {\iota}$ be given.
Let $ plus, mult : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{\iota}}}$ be given.
{\bf{Notation.}} We use $\inflc$ as a right associative infix operator  corresponding to applying term ${plus}$.
{\bf{Notation.}} We use $\infkc$ as a right associative infix operator  corresponding to applying term ${mult}$.
\begin{definition}\label{def:fgihahmgjgdgjgehpfgejgfgmgeg}
$\mname{explicit\_Field}$ is the opaque object of type ${o}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 32dcc27d27b5003a86f8b13ba9ca16ffaec7168a11c5d9850940847c48148591 \\
Pure Object Address: & TMbJPQHnQf1mY3onQrsrhqCR24yapErnf21 \\
Theory Object Id: & 0020dc091a770bc26640d405438dea5752e187e4f46e3ea423aa06fbf99169cd \\
Theory Object Address: & TMctGNriWgkHut2Cii7sum1tGGmeJ1TQf2z
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
explicit_Field_I
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfje} 
$$
\begin{array}{c}
{{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}+{{y}}}} \in {{R}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}+{{({{{{y}}+{{z}}}})}}}}={{{{({{{{x}}+{{y}}}})}}+{{z}}}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}+{{y}}}}={{{{y}}+{{x}}}}}}}})}}}{\unicdbdjdcd}\\
{{{{{zero}} \in {{R}}}}}{\unicdbdjdcd}{{{({{\unicdcdadad x \in {{R}} .  {{{{{{zero}}+{{x}}}}={{x}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x \in {{R}} .  {{\unicdcdaddd y \in {{R}} .  {{{{{{x}}+{{y}}}}={{zero}}}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}*{{y}}}} \in {{R}}}}}})}}}{\unicdbdjdcd}\\
{{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}*{{({{{{y}}*{{z}}}})}}}}={{{{({{{{x}}*{{y}}}})}}*{{z}}}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}*{{y}}}}={{{{y}}*{{x}}}}}}}})}}}{\unicdbdjdcd}{{{({{{{one}} \in {{R}}}})}}}{\unicdbdjdcd}{{{({{{{one}}\unicdcdgdad{{zero}}}})}}}{\unicdbdjdcd}\\
{{{({{\unicdcdadad x \in {{R}} .  {{{{{{one}}*{{x}}}}={{x}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x \in {{R}} .  {{{{{{x}}\unicdcdgdad{{zero}}}}\unicdbdjdcd{{\unicdcdaddd y \in {{R}} .  {{{{{{x}}*{{y}}}}={{one}}}}}}}}}})}}}{\unicdbdjdcd}\\
{{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}*{{({{{{y}}+{{z}}}})}}}}={{{{{{x}}*{{y}}}}+{{{{x}}*{{z}}}}}}}}}})}}}{\unicdbdjdcd}{{\mname{{explicit\_Field}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3ccc525dac877738bde04411aa5b2802762d08d54c0801938fbdb890674a0002 \\
Pure Prop Address: & TMdJ9fH9ZyRuWnaU1MAQEZ1tDGUfPtL2cec \\
Theory Prop Id: & 51ce1195007755d317528633fca294788000229835b66559cc3f47f888639540 \\
Theory Prop Address: & TMKFU5TXhW1AbfR8o181j3pjJGyWs64AHai
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Field_E
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpffe} 
$$
\begin{array}{c}
{\unicdcdadad q : }{{{o}}}{ .  }\\
({{\mname{{explicit\_Field}}}}\unicdbdjdcd\\
{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}+{{y}}}} \in {{R}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}+{{({{{{y}}+{{z}}}})}}}}={{{{({{{{x}}+{{y}}}})}}+{{z}}}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}+{{y}}}}={{{{y}}+{{x}}}}}}}})}}\unicdbdjdcd\\
{{({{{{zero}} \in {{R}}}})}}\unicdbdjdcd{{({{\unicdcdadad x \in {{R}} .  {{{{{{zero}}+{{x}}}}={{x}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x \in {{R}} .  {{\unicdcdaddd y \in {{R}} .  {{{{{{x}}+{{y}}}}={{zero}}}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}*{{y}}}} \in {{R}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}*{{({{{{y}}*{{z}}}})}}}}={{{{({{{{x}}*{{y}}}})}}*{{z}}}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}*{{y}}}}={{{{y}}*{{x}}}}}}}})}}\unicdbdjdcd\\
{{({{{{one}} \in {{R}}}})}}\unicdbdjdcd{{({{{{one}}\unicdcdgdad{{zero}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x \in {{R}} .  {{{{{{one}}*{{x}}}}={{x}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x \in {{R}} .  {{{{{{x}}\unicdcdgdad{{zero}}}}\unicdbdjdcd{{\unicdcdaddd y \in {{R}} .  {{{{{{x}}*{{y}}}}={{one}}}}}}}}}})}}\unicdbdjdcd\\
{{{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}*{{({{{{y}}+{{z}}}})}}}}={{{{{{x}}*{{y}}}}+{{{{x}}*{{z}}}}}}}}}})}}\unicdbdjdcd{{q}}}}\\
{\unicdbdjdcd}{{{\mname{{explicit\_Field}}}}}{\unicdbdjdcd}{q}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & bb3db9eded830bf9d92132c0016be1d1a259929bceda5bdf57b4f64fcba43184 \\
Pure Prop Address: & TMXJPRqy8mBTRo6EPJpYzNS1rE86xJ2ABjo \\
Theory Prop Id: & 6c4aa1700c811949523aab7956f68644700f9d543e3915471880f5956881b35e \\
Theory Prop Address: & TMcxwBH2nbJB8F5LxJwz4A2as2v9Ejx9zoD
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:fgihahmgjgdgjgehpfgejgfgmgegpfngjgogfhdh}
$\mname{explicit\_Field\_minus}$ is the opaque object of type ${{\iota}\unicdbdjdcd{\iota}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 5be570b4bcbe7fefd36c2057491ddcc7b11903d8d98ca54d9b37db60d1bf0f7e \\
Pure Object Address: & TMMPF8zir9fkfAtJFGxe63EcXTEPLHDtBA4 \\
Theory Object Id: & 7a10c2aa3843a7152cec6319a52f2f9ff01bb82b441aed667fd99a775dab9980 \\
Theory Object Address: & TMYcEMbnauFAYpJxp2DpEB5nscfUnNcsbZy
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\prenc{-}$ as a prefix operator  corresponding to applying term ${\mname{explicit\_Field\_minus}}$.
\begin{verbatim}
explicit_Field_minus_prop
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfngjgogfhdhpfahchpgah} ${{\mname{explicit\_Field}}\unicdbdjdcd{\unicdcdadad x \in {R} .  {{{\prenc{{x}}} \in {R}}\unicdcdcdhd{{{x}+{\prenc{{x}}}}={zero}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & dfdfb501a72ee10c72ad8933d6f1bd3d1d25a2009a655a5683cf351539aa70bc \\
Pure Prop Address: & TMRiffBv5SK7Dv3GZ8Qc3WgwrC1MxCSpHC7 \\
Theory Prop Id: & be5356f76e63b2d1a7cc20f125e927198f6005afc05464565ca4304115a8e435 \\
Theory Prop Address: & TMKQfrW9q8xeEbq3YsFtzRuMpXJcsRviQhq
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Field_minus_clos
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfngjgogfhdhpfdgmgpgdh} ${{\mname{explicit\_Field}}\unicdbdjdcd{\unicdcdadad x \in {R} .  {{\prenc{{x}}} \in {R}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 19192856a86a06ac1d56d571d172b3dd60e77b95edea0e5a195a7849ea9fdd1d \\
Pure Prop Address: & TMLDrc2xd6CY9VqXqvmt3SZypH79h73yzYt \\
Theory Prop Id: & 853f414afb3b6db2964375b75fc2bdfa06eba2d8a9cf8c7993e79be8c16c241c \\
Theory Prop Address: & TMMd78EndbrgewWKg7cug4aFmuNLcdvLETi
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Field_minus_R
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfngjgogfhdhpfcf} ${{\mname{explicit\_Field}}\unicdbdjdcd{\unicdcdadad x \in {R} .  {{{x}+{\prenc{{x}}}}={zero}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 16bd02b0d5c539b89ab6c3b290f99da455cb893382173ba554e3a9499850d228 \\
Pure Prop Address: & TMWcY3CmCi3C7TchQ2ZWaU2w6UYvY5EyRBX \\
Theory Prop Id: & e00e5ccf74077747e0399d61c172ce48cfbd48eee9e6d1a7ccc3d55adb0814dd \\
Theory Prop Address: & TMJphf6VbWpCYsxdqnUTWXSj422gfKJmxEo
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Field_minus_L
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfngjgogfhdhpfme} ${{\mname{explicit\_Field}}\unicdbdjdcd{\unicdcdadad x \in {R} .  {{{\prenc{{x}}}+{x}}={zero}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1e484c596156e799c8b1be02b2f184d891d04b570a626b0f353d58fb19b04a98 \\
Pure Prop Address: & TMZbY42rURTo9ZUysPTCKb3htjwFZXbEw1T \\
Theory Prop Id: & 3c1cf77f15777c38163c09cb6f75c87835fac72965b443566fab8a7a40e9665f \\
Theory Prop Address: & TMYDLj9BQtJLVtxTosQ1aMz4YRJvYdWceaV
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Field_plus_cancelL
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfahmgfhdhpfdgbgogdgfgmgme} ${{\mname{explicit\_Field}}\unicdbdjdcd{\unicdcdadad x y z \in {R} .  {{{{x}+{y}}={{x}+{z}}}\unicdbdjdcd{{y}={z}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b9cc3f21432ad1dcc45524e4ac02e5182053a3f7477ca552e87c5132962558cb \\
Pure Prop Address: & TMLW7dUp3ubrm2KQb1j1qqXX7SiHc2FMGYH \\
Theory Prop Id: & da9a6bc0e051dd48f33393f832d94859ae59087f843e5647b7d48be40b16752c \\
Theory Prop Address: & TMGDxEVrun2MVRqLiWkibA4xgq5mXZYRefM
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Field_plus_cancelR
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfahmgfhdhpfdgbgogdgfgmgcf} ${{\mname{explicit\_Field}}\unicdbdjdcd{\unicdcdadad x y z \in {R} .  {{{{x}+{z}}={{y}+{z}}}\unicdbdjdcd{{x}={y}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 8e7410c2408dd9fc6349ca4ae571c9cfc54c4cdbd647f030a422a0f138d33342 \\
Pure Prop Address: & TMLaB8tvdGpW8DwHyHVQH6BkFA5qABz62Xw \\
Theory Prop Id: & 148a14870a33e0b1322a50fde11a6ff30e6ed7d2cf59e7b846b0a4fece952554 \\
Theory Prop Address: & TMdwAiT4yYz4w2xxTmzsG9vifx1CtnVpbbK
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Field_minus_invol
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfngjgogfhdhpfjgogghpgmg} ${{\mname{explicit\_Field}}\unicdbdjdcd{\unicdcdadad x \in {R} .  {{\prenc{{\prenc{{x}}}}}={x}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d9245973a06673bbaca0fe2244ae2b76cb719974a7a1a5be04c9786c8ccd521a \\
Pure Prop Address: & TMSFpQWK1zrTS89dhaG5MbKGZ3CzKuw2Hez \\
Theory Prop Id: & e4a26d2ce9a3a793e18ddeb34b9e5f5689c952c20c234bbeaccb1e36b6ed3934 \\
Theory Prop Address: & TMSuivsorWRWJ8izeRUNUJJmCYigXx7CwUM
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Field_minus_one_In
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfngjgogfhdhpfpgogfgpfjeog} ${{\mname{explicit\_Field}}\unicdbdjdcd{{\prenc{{one}}} \in {R}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3dea9f1e7c156a2c2a714f0dcbe2bb48e13a8f0786132f71784621f4566ba3de \\
Pure Prop Address: & TMKembKWo9bsc7rvXjS3b9tPDernwnfN69C \\
Theory Prop Id: & c3141394b9d6650476539d3de9c24c2094fafd277233c838e05eece229179706 \\
Theory Prop Address: & TMYYz1ipvpJRoYVLBTTHwW5inLAqHEZJNZj
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Field_zero_multR
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfkhfgchpgpfngfhmgehcf} ${{\mname{explicit\_Field}}\unicdbdjdcd{\unicdcdadad x \in {R} .  {{{x}*{zero}}={zero}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & f6ea109454bd63c383487f79cde58c39e60809206cdeecfb0cf5c33ba7a39a78 \\
Pure Prop Address: & TMc9K3rxpDhdcV4fiwudpCAvCbo4EgSX2FM \\
Theory Prop Id: & cddbcdbd4bc296b7c12e6e905456a622a658af38644ec81e091b58a94847904f \\
Theory Prop Address: & TMTpJuV9Dgs6cEeCYFcQ71NUT9zLc55yQ6G
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Field_zero_multL
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfkhfgchpgpfngfhmgehme} ${{\mname{explicit\_Field}}\unicdbdjdcd{\unicdcdadad x \in {R} .  {{{zero}*{x}}={zero}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & a6219e7c7ce408f1a4ed2d0bbb6897dd8a32479b32efbe9caa5735d0b3fe8fa2 \\
Pure Prop Address: & TMbHRokQ9EFeZHPhTtnpAgJYqraYBTYVR9D \\
Theory Prop Id: & bf3f6a5eb75519377a3a0ab3681dee400b8bb378f33c7dc4dcd864f874a61fca \\
Theory Prop Address: & TMWNakNQV1Rea25NYbFjsGGZVZqZY7C1sHo
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Field_minus_mult
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfngjgogfhdhpfngfhmgeh} ${{\mname{explicit\_Field}}\unicdbdjdcd{\unicdcdadad x \in {R} .  {{\prenc{{x}}}={{({\prenc{{one}}})}*{x}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & b725ff0fba328afa96eaf8d8cee4c89ac94d1e750fd3006aba3b6f6f6dc8d6fa \\
Pure Prop Address: & TMTsU5wxazHBfmvDRU6dzpmJe6y8taJi1zr \\
Theory Prop Id: & 6c32dff82b3955c923f8ad0af52f709a8d9750b5932c46a80584bf6fe86d4079 \\
Theory Prop Address: & TMG8caBgEaUDhsJtbdypcFcgYXKH7VumZf2
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Field_minus_one_square
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfngjgogfhdhpfpgogfgpfdhbhfhbgchfg} ${{\mname{explicit\_Field}}\unicdbdjdcd{{{({\prenc{{one}}})}*{({\prenc{{one}}})}}={one}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 33687daadedd9048924a66186e9b1d11d2849f1c4c403989aa1dde1a2c8d1839 \\
Pure Prop Address: & TMRYgfX4tEirAsP8NiXBD231RunzNSeTGaQ \\
Theory Prop Id: & 81b69b4f65a19abefefc96e03e44e28ccab7aa2d8fdd98ec035a25ceeb9f9c01 \\
Theory Prop Address: & TMWNc4GkfcpRjYQn5ss6k1srmNCX8pS3RTW
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Field_minus_square
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfngjgogfhdhpfdhbhfhbgchfg} ${{\mname{explicit\_Field}}\unicdbdjdcd{\unicdcdadad x \in {R} .  {{{({\prenc{{x}}})}*{({\prenc{{x}}})}}={{x}*{x}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & db0127263baf3b745b4b535f56b1f7c123744b30c2db578852e18d3b417f004c \\
Pure Prop Address: & TMTV85Vo7eTyFBiu5YCvAEyGtkJGhZnmztE \\
Theory Prop Id: & cc20f4507a4b8ab01b79ded3da8b0945e39532ee96a70c6ef10bab5a6e176273 \\
Theory Prop Address: & TMFLG2o5FZ3crQm2waGZhJKk41t1KZmfnsC
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Field_minus_zero
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfngjgogfhdhpfkhfgchpg} ${{\mname{explicit\_Field}}\unicdbdjdcd{{\prenc{{zero}}}={zero}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 677fffd7ef5af74d4eaf3075a3db01ed4e7685052f86b5da66de86c40ac0029c \\
Pure Prop Address: & TMbHTa1NSQxgViQGA5LgQhajneJu1oTW2n7 \\
Theory Prop Id: & d58ae486546dede085e27a56fa6854b755e9bfc2f0b3c78aa184624c4d4535e2 \\
Theory Prop Address: & TMHxghZtCQFNpCShXEagGPGXBetd1ZxTcCB
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Field_dist_R
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfegjgdhehpfcf} ${{\mname{explicit\_Field}}\unicdbdjdcd{\unicdcdadad x y z \in {R} .  {{{({{x}+{y}})}*{z}}={{{x}*{z}}+{{y}*{z}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & de79567ee223c72fabfe843b7d7526a3a12428317b799a662ff4ce3ad76f9472 \\
Pure Prop Address: & TMMz7KwL6xBwXeCscdhDKUbgZEeMqZXz2n1 \\
Theory Prop Id: & 2a896a6970c2a6f3d291e0b5a6330cabecc63ba17b6f9f6b4338f1a0e03a08a0 \\
Theory Prop Address: & TMXM5285AmLUf7pvii4Ym8YsRizGaSngE2Z
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Field_minus_plus_dist
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfngjgogfhdhpfahmgfhdhpfegjgdheh} ${{\mname{explicit\_Field}}\unicdbdjdcd{\unicdcdadad x y \in {R} .  {{\prenc{{({{x}+{y}})}}}={{\prenc{{x}}}+{\prenc{{y}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7c28f73f41fb9362c802db194a80e809ab40b5fcbf86889187a241fb04c45f07 \\
Pure Prop Address: & TMMbYxMRKezKTJauH5tFeT6YcdVqNqaoNyb \\
Theory Prop Id: & 3477df803cb462a1c67676532b809a8085f5965e8eded20de22c081f8b380c1f \\
Theory Prop Address: & TMJEy6ntH8yniiQ1XpVapukWC9af7szg259
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Field_minus_mult_L
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfngjgogfhdhpfngfhmgehpfme} ${{\mname{explicit\_Field}}\unicdbdjdcd{\unicdcdadad x y \in {R} .  {{{({\prenc{{x}}})}*{y}}={\prenc{{({{x}*{y}})}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & d4042ab05af8694ed9f50ea48d73fd8241fe9e096a57f64ca3767ec2ee8622b8 \\
Pure Prop Address: & TMMDqKcMu6spUHkosKvvDfVjBChv657VpPo \\
Theory Prop Id: & 2c1cad10f4a09ca8c4864cae7b040bf84788c98182553b04deca95d667a74739 \\
Theory Prop Address: & TMb8pKtSFLQTYNxrQHoTXXs92fMEGh22svD
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Field_minus_mult_R
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfngjgogfhdhpfngfhmgehpfcf} ${{\mname{explicit\_Field}}\unicdbdjdcd{\unicdcdadad x y \in {R} .  {{{x}*{({\prenc{{y}}})}}={\prenc{{({{x}*{y}})}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1c896cfcf91413c6c45f35892ce57731b0adad535619672d8857f0281523657a \\
Pure Prop Address: & TMHHkG7bnn6fLtxgsof8vd6CC3u39fp5sYn \\
Theory Prop Id: & 46e01b365cf641485dae65460ad1681ecaab879cc9dd36e6f2dc58b3a94a1cd0 \\
Theory Prop Address: & TMPM6UjftWZ8u7qznYUZoTw3xxFGQZUT3ce
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Field_square_zero_inv
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfdhbhfhbgchfgpfkhfgchpgpfjgoggh} ${{\mname{explicit\_Field}}\unicdbdjdcd{\unicdcdadad x \in {R} .  {{{{x}*{x}}={zero}}\unicdbdjdcd{{x}={zero}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 18939b3ff00eabb11a4a28ae19cc0aac425c72704752d525860f80dfe5375212 \\
Pure Prop Address: & TMNAKKNruWjcXkrAW9Rb6BxwgJg9jKX4Lbd \\
Theory Prop Id: & fe699ea22147eff4c7086ff7bf4954794c5e61d9d3e22c587a86681568f2423d \\
Theory Prop Address: & TMP55pVZRC8XUcxBEuENBHAqrd7cau5uiY4
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Field_mult_zero_inv
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfgejgfgmgegpfngfhmgehpfkhfgchpgpfjgoggh} 
$$
\begin{array}{c}
{{{\mname{{explicit\_Field}}}}}{\unicdbdjdcd}{\unicdcdadad x y \in }{{{R}}}{ .  }{{{{{{{x}}*{{y}}}}={{zero}}}}}{\unicdbdjdcd}{{{{{{x}}={{zero}}}}\unicdcdcdid{{{{y}}={{zero}}}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 48f3d685f5c19ffb943e4e92bf1143cd300504313d7025cbcd85d11fa57e29aa \\
Pure Prop Address: & TMMoGSv87AzopLCYaS7tpk3DNioBcaw6e6Z \\
Theory Prop Id: & d90b744848de4a3c083b3ce57e25e069c0d9b625f137f9e544dde929638e2794 \\
Theory Prop Address: & TManTc7e6UWwgQhhz3U1c3VVG946TvLTxR9
\end{tabular}
\end{center}

\end{theorem}
Let $ leq : {{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ be given.
{\bf{Notation.}} We use $\infmdnd$ as an infix operator  corresponding to applying term ${leq}$.
\begin{definition}\label{def:fgihahmgjgdgjgehpfpechegfgchfgeggejgfgmgeg}
$\mname{explicit\_OrderedField}$ is the opaque object of type ${o}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & a18f7bca989a67fb7dc6df8e6c094372c26fa2c334578447d3314616155afb72 \\
Pure Object Address: & TMSMYTTginXTnkcVZtpjAKPAaL7BnqqgRds \\
Theory Object Id: & eea7fafdf682c37d08f8505d8389845b96987326a92b0823dac083b00eda754c \\
Theory Object Address: & TMUVEidBNjgBhKRvbJD1JJ2kD28DQi7APKy
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
explicit_OrderedField_I
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfpechegfgchfgeggejgfgmgegpfje} 
$$
\begin{array}{c}
  {{{\mname{{explicit\_Field}}}}}{\unicdbdjdcd}{{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}\unicdcdgded{{y}}}}\unicdbdjdcd{{{{{{y}}\unicdcdgded{{z}}}}\unicdbdjdcd{{{{x}}\unicdcdgded{{z}}}}}}}}}})}}}{\unicdbdjdcd}\\
  {{{({{\unicdcdadad x y \in {{R}} .  {{{{{{{{x}}\unicdcdgded{{y}}}}\unicdcdcdhd{{{{y}}\unicdcdgded{{x}}}}}}\unicdbdjded{{{{x}}={{y}}}}}}}})}}}{\unicdbdjdcd}\\
{{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}\unicdcdgded{{y}}}}\unicdcdcdid{{{{y}}\unicdcdgded{{x}}}}}}}})}}}{\unicdbdjdcd}{{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}\unicdcdgded{{y}}}}\unicdbdjdcd{{{{{{x}}+{{z}}}}\unicdcdgded{{{{y}}+{{z}}}}}}}}}})}}}{\unicdbdjdcd}\\
{{{({{\unicdcdadad x y \in {{R}} .  {{{{{{zero}}\unicdcdgded{{x}}}}\unicdbdjdcd{{{{{{zero}}\unicdcdgded{{y}}}}\unicdbdjdcd{{{{zero}}\unicdcdgded{{{{x}}*{{y}}}}}}}}}}}})}}}{\unicdbdjdcd}{{\mname{{explicit\_OrderedField}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 80eb1d0d6d1ae59e7716b600362a8edadf3a3d46606eefe17eb4379546b5b255 \\
Pure Prop Address: & TMVbN3H3LfjoJc5JN3kFVvxfeyGkhWvjBwf \\
Theory Prop Id: & 71586c9655f0d1781fbbb7e18105c89958843a5ccb8e7deeffe6b9e62b1b1e09 \\
Theory Prop Address: & TMTVD1npwX9pr1azvDC9toE4RLXrqq7MsyC
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_OrderedField_E
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfpechegfgchfgeggejgfgmgegpffe} 
$$
\begin{array}{c}
{\unicdcdadad q : }{{{o}}}{ .  }\\
({{\mname{{explicit\_OrderedField}}}}\unicdbdjdcd{{\mname{{explicit\_Field}}}}\unicdbdjdcd\\
{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}\unicdcdgded{{y}}}}\unicdbdjdcd{{{{{{y}}\unicdcdgded{{z}}}}\unicdbdjdcd{{{{x}}\unicdcdgded{{z}}}}}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y \in {{R}} .  {{{{{{{{x}}\unicdcdgded{{y}}}}\unicdcdcdhd{{{{y}}\unicdcdgded{{x}}}}}}\unicdbdjded{{{{x}}={{y}}}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y \in {{R}} .  {{{{{{x}}\unicdcdgded{{y}}}}\unicdcdcdid{{{{y}}\unicdcdgded{{x}}}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x y z \in {{R}} .  {{{{{{x}}\unicdcdgded{{y}}}}\unicdbdjdcd{{{{{{x}}+{{z}}}}\unicdcdgded{{{{y}}+{{z}}}}}}}}}})}}\unicdbdjdcd\\
{{{{({{\unicdcdadad x y \in {{R}} .  {{{{{{zero}}\unicdcdgded{{x}}}}\unicdbdjdcd{{{{{{zero}}\unicdcdgded{{y}}}}\unicdbdjdcd{{{{zero}}\unicdcdgded{{{{x}}*{{y}}}}}}}}}}}})}}\unicdbdjdcd{{q}}}})\\
{\unicdbdjdcd}{{{\mname{{explicit\_OrderedField}}}}}{\unicdbdjdcd}{q}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 1c269ba4e553561a1cc6de2a41b6545ec8ac75e48e3c6cb23b2b6a324a64952b \\
Pure Prop Address: & TMVNKTpEnn5zTRZtpuHVXwYgJDgVq64jhQb \\
Theory Prop Id: & 5c835e8cb20f579d989cd542e60e75f77e9b09c2976f6070c05a17cfca4d407a \\
Theory Prop Address: & TMaCBRHe1Qvk5uX74Rit6toSqNPaYfiTK4D
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_OrderedField_minus_leq
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfpechegfgchfgeggejgfgmgegpfngjgogfhdhpfmgfgbh} ${{\mname{explicit\_OrderedField}}\unicdbdjdcd{\unicdcdadad x y \in {R} .  {{{x}\unicdcdgded{y}}\unicdbdjdcd{{\prenc{{y}}}\unicdcdgded{\prenc{{x}}}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0d0f5cad7897b1fc9859fb0fb353f392e444d5b3b7e1db20a4f125e0e21ce6bf \\
Pure Prop Address: & TMMwfqJswL3g7Cij23YHpxZpvqT7KfRqNMe \\
Theory Prop Id: & ee304f2ce86cb10f1be68e56828aad0317279e773397f75e93647653c83be151 \\
Theory Prop Address: & TMMzgVBuTQhmpTV2B9ybeJX6tiEkbUXhbe3
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_OrderedField_square_nonneg
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfpechegfgchfgeggejgfgmgegpfdhbhfhbgchfgpfogpgogogfghg} ${{\mname{explicit\_OrderedField}}\unicdbdjdcd{\unicdcdadad x \in {R} .  {{zero}\unicdcdgded{{x}*{x}}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & ebf414f2c6ff9848d35121369f85472ab25e8af5cc2728af838e40787e67ac6f \\
Pure Prop Address: & TMV8VUHDk12iC7xpNnNDLjZD9BtuYf7ESyK \\
Theory Prop Id: & 891e8662d8b95f38bd875c846330ed8d495c4375ade2fe5aac04a6d4c9daa3d3 \\
Theory Prop Address: & TMJ9LeAui7MyNuXXvPgJDye1dzUzpzKZanv
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_OrderedField_sum_squares_nonneg
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfpechegfgchfgeggejgfgmgegpfdhfhngpfdhbhfhbgchfgdhpfogpgogogfghg} 
${{{\mname{{explicit\_OrderedField}}}}}{\unicdbdjdcd}{\unicdcdadad x y \in }{{{R}}}{ .  }{{{{zero}}\unicdcdgded{{{{{{x}}*{{x}}}}+{{{{y}}*{{y}}}}}}}}$.
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 7596b76c40f5977c5d12346563941ea1bd17dedf0fdc6d4677b21fd667046cd0 \\
Pure Prop Address: & TMXYnd1YrHHrvjWcoZ6XYMkRe7mUtnUsHMB \\
Theory Prop Id: & d9447e2431709c9a2271ba5d7c8d2c42675d962980e8d0c6a945b47a84e3f7f2 \\
Theory Prop Address: & TMR3ypJ2YAEpeYUYejDaWcqzkgc8VHN9BYU
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_OrderedField_sum_nonneg_zero_inv
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfpechegfgchfgeggejgfgmgegpfdhfhngpfogpgogogfghgpfkhfgchpgpfjgoggh} 
$$
\begin{array}{c}
{{{\mname{{explicit\_OrderedField}}}}}{\unicdbdjdcd}{\unicdcdadad x y \in }{{{R}}}{ .  }{{{{{zero}}\unicdcdgded{{x}}}}}{\unicdbdjdcd}{{{{{zero}}\unicdcdgded{{y}}}}}{\unicdbdjdcd}{{{{{{{x}}+{{y}}}}={{zero}}}}}{\unicdbdjdcd}\\
{{{{{{x}}={{zero}}}}\unicdcdcdhd{{{{y}}={{zero}}}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 072f56b723bef4ade29f644b20f32711dd9f8872653a4603191255a02ed12aa5 \\
Pure Prop Address: & TMbqPNKUAZHZZvbj8kXQXLfL56CpAozuS97 \\
Theory Prop Id: & 5f6c78eb0411a6fb156cf3b2848ebb0c759d7a6a6b653d97dec27052916e94e5 \\
Theory Prop Address: & TMXUo7T7pnNdX24nuWLNaNSHmUgB2UFnGt4
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_OrderedField_sum_squares_zero_inv
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfpechegfgchfgeggejgfgmgegpfdhfhngpfdhbhfhbgchfgdhpfkhfgchpgpfjgoggh} 
$${{{\mname{{explicit\_OrderedField}}}}}{\unicdbdjdcd}{\unicdcdadad x y \in }{{{R}}}{ .  }{{{{{{{{{x}}*{{x}}}}+{{{{y}}*{{y}}}}}}={{zero}}}}}{\unicdbdjdcd}{{{{{{x}}={{zero}}}}\unicdcdcdhd{{{{y}}={{zero}}}}}}.$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 3475f408fb7b3dec70f825cb0332b28e033d25bc6e4cbd6a9b382bbd3d531484 \\
Pure Prop Address: & TMGde3gx4w4Uh9Awwi1qwfiWQ4CBJfJAtS1 \\
Theory Prop Id: & 5736f60e1ddc12d7525825b06f528d3d62fe1e6481630bd0d8e030f123c54b60 \\
Theory Prop Address: & TMG76tdh9rhRwpDqWUkbVYQDxYySTKTuYYE
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_OrderedField_leq_refl
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfpechegfgchfgeggejgfgmgegpfmgfgbhpfchfgggmg} ${{\mname{explicit\_OrderedField}}\unicdbdjdcd{\unicdcdadad x \in {R} .  {{x}\unicdcdgded{x}}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 6d89bac73c97399406da5761a4e05ca142b2af3c9ea45f75c5674037832d0352 \\
Pure Prop Address: & TMJPTfciQTSdnS3SFhTmePpEG61KkYyXyh8 \\
Theory Prop Id: & 915e8fb0a5a50db0b4874494c5e1fbe27f4a9e913998db7bdbe6335c2782cef8 \\
Theory Prop Address: & TMUeqaV9ny8ooGx2mDKgZUyR36krjn7twu6
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_OrderedField_leq_antisym
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfpechegfgchfgeggejgfgmgegpfmgfgbhpfbgogehjgdhjhng} 
${{{\mname{{explicit\_OrderedField}}}}}{\unicdbdjdcd}{\unicdcdadad x y \in }{{{R}}}{ .  }{{{{{x}}\unicdcdgded{{y}}}}}{\unicdbdjdcd}{{{{{y}}\unicdcdgded{{x}}}}}{\unicdbdjdcd}{{{{x}}={{y}}}}$.
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 92c2c21b46e137352ea2b13877fba3bccf89bb379a6f9cb05d766c8493fbc378 \\
Pure Prop Address: & TMdF3uckvYNFsZLo2N2AUXRf961iqhpb4nY \\
Theory Prop Id: & 2313aae88e7fee79d5231f7afbc5542b995b3af3ba7cc654b0066c73120152d4 \\
Theory Prop Address: & TMNmtcpgnXCEWQdjZhJoxe1nhrEE87jGdwk
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_OrderedField_leq_tra
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfpechegfgchfgeggejgfgmgegpfmgfgbhpfehchbg} 
${{{\mname{{explicit\_OrderedField}}}}}{\unicdbdjdcd}{\unicdcdadad x y z \in }{{{R}}}{ .  }{{{{{x}}\unicdcdgded{{y}}}}}{\unicdbdjdcd}{{{{{y}}\unicdcdgded{{z}}}}}{\unicdbdjdcd}{{{{x}}\unicdcdgded{{z}}}}$.
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 2d02678a2209fd726235ddb09c2aa9290b48375519487773c818f9d57860c62b \\
Pure Prop Address: & TMcsuosBpLY4AFhGspmWx2rN1cH12b2XPqe \\
Theory Prop Id: & 642b84d1691774bc188f593803d0d85f1012bda7c66ff4ef994e821e3570a030 \\
Theory Prop Address: & TMNgAZiMJeVFoYAuFpPJez3pVME9zrth8Xd
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_OrderedField_leq_zero_one
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfpechegfgchfgeggejgfgmgegpfmgfgbhpfkhfgchpgpfpgogfg} ${{\mname{explicit\_OrderedField}}\unicdbdjdcd{{zero}\unicdcdgded{one}}}$. The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 4f14f3aee0dd811396902d2e346ed9447d586fecfa610cb7f80d8c018b78445c \\
Pure Prop Address: & TMcxPXzviwMyx5FiSvb9JnufFyGPAdVhiA2 \\
Theory Prop Id: & a0dbd6bf9eb8bf6f8529771cbf53aa3be49e04449a97763b5e01ea7d7ea2a870 \\
Theory Prop Address: & TMGr9TnXkfhuvkbv1dMj5JtTZ8RSfzoP95A
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:mgeh}
We define $\mname{lt}$ to be ${\uniddcgcg x y .  {{{x}\unicdcdgded{y}}\unicdcdcdhd{{x}\unicdcdgdad{y}}}}$ of type ${{\iota}\unicdbdjdcd{{\iota}\unicdbdjdcd{o}}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & d326e5351e117c7374d055c5289934dc3a6e79d66ed68f1c6e23297feea0148e \\
Pure Object Address: & TMGFyhEzMLotVozJF1yiunrkGLuFdfjWkng \\
Theory Object Id: & f91dfd2380597226f5c8900812832b2a5a67ae6568fe2b2a605848bd8d22540a \\
Theory Object Address: & TMcecisvAF6JJ66jafWS8ZR87w7SMBwYATJ
\end{tabular}
\end{center}

\end{definition}
{\bf{Notation.}} We use $\infmd$ as an infix operator  corresponding to applying term ${\mname{lt}}$.
\begin{definition}\label{def:ogbgehpeggpechegfgchfgeggejgfgmgegpfah}
$\mname{natOfOrderedField\_p}$ is the opaque object of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & f1c45e0e9f9df75c62335865582f186c3ec3df1a94bc94b16d41e73bf27899f9 \\
Pure Object Address: & TMUGM8F7ocg9jGYhPZVwzCfNfPzPmAanw4Z \\
Theory Object Id: & f89652d7f0e1787e89129826561eeccb4f5558676c7910ea999306a32285e218 \\
Theory Object Address: & TMFAmRM27u8JLyZ7Jf1HAC8DeSELjytd8Ua
\end{tabular}
\end{center}

\end{definition}
Let $N$ be ${\{n \in {R}|{{\mname{natOfOrderedField\_p}}~{n}}\}}$.
Let $Npos$ be ${\{n \in {N}|{{n}\unicdcdgdad{zero}}\}}$.
\begin{verbatim}
explicit_Nats_natOfOrderedField
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfoebgehdhpfogbgehpeggpechegfgchfgeggejgfgmgeg} 
$$
\begin{array}{c}
{{{\mname{{explicit\_OrderedField}}}}}{\unicdbdjdcd}{{{{{{{{\mname{{explicit\_Nats}}}}~{{N}}}}~{{zero}}}}~{{({{\uniddcgcg m .  {{{{m}}+{{one}}}}}})}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 9cb324808fc5cf72d2d653a2418ab30cb9b85476e00be35fcd9b57f1bb93ad72 \\
Pure Prop Address: & TMWcMhihbJqy1w5uYhuM3Es9nEdDsCM8SJn \\
Theory Prop Id: & 8d1a312e7d98b7df2205e4cfa93c99a5f6dfa4019921c333b9d177cc70aca004 \\
Theory Prop Address: & TMZXnwRs21hpHmTpXy9R1JnG8n2ykq4d1cS
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_PosNats_natOfOrderedField
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfafpgdhoebgehdhpfogbgehpeggpechegfgchfgeggejgfgmgeg} 
$$
\begin{array}{c}
{{{\mname{{explicit\_OrderedField}}}}}{\unicdbdjdcd}{{{{{{{{\mname{{explicit\_Nats}}}}~{{Npos}}}}~{{one}}}}~{{({{\uniddcgcg m .  {{{{m}}+{{one}}}}}})}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 36987abea2f716243c8b427e45e8b2e1ae58f4dd9e1dd000b423f2e6f4bc48a0 \\
Pure Prop Address: & TMWy3odsbnhVAitSJ5hzGBv9T8fmV4ZP3S7 \\
Theory Prop Id: & 7b42ab4ebcb5779370bac576623544325cab108670d64b30ebe19743a3fa9054 \\
Theory Prop Address: & TMZEMUgieWVVNR5ysQcJpnbXL1KpnZvBLMh
\end{tabular}
\end{center}

\end{theorem}
Let $Z$ be ${\{n \in {R}|{{{{\prenc{{n}}} \in {Npos}}\unicdcdcdid{{n}={zero}}}\unicdcdcdid{{n} \in {Npos}}}\}}$.
\begin{definition}\label{def:fgihahmgjgdgjgehpfpechegfgchfgeggejgfgmgegpfchbgehjgpgogbgmgah}
We define $\mname{explicit\_OrderedField\_rationalp}$ to be $${\uniddcgcg x .  {\unicdcdaddd n \in {Z} .  {\unicdcdaddd m \in {Npos} .  {{{m}*{x}}={n}}}}}$$ of type ${{\iota}\unicdbdjdcd{o}}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & bacdefb214268e55772b42739961f5ea4a517ab077ed4b168f45f4c3d4703ec4 \\
Pure Object Address: & TMS9Jk69fwzyerTVyhC5cLftFrz8QwxR86G \\
Theory Object Id: & 6449a4f053483876d454bb93a1566cd7b4d24332ae6e750097943c2e903e0426 \\
Theory Object Address: & TMdsiVayo81K6oYHmqnGdSi5QMPLt3MnzCJ
\end{tabular}
\end{center}

\end{definition}
Let $Q$ be ${\{x \in {R}|{{\mname{explicit\_OrderedField\_rationalp}}~{x}}\}}$.
\begin{verbatim}
explicit_OrderedField_Npos_props
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfpechegfgchfgeggejgfgmgegpfoeahpgdhpfahchpgahdh} 
$$
\begin{array}{c}
{{{\mname{{explicit\_OrderedField}}}}}{\unicdbdjdcd}{\unicdcdadad p : }{{{o}}}{ .  }\\
({{{{Npos}} \subseteq {{R}}}}\unicdbdjdcd{{{{{{{{\mname{{explicit\_Nats}}}}~{{Npos}}}}~{{one}}}}~{{({{\uniddcgcg m .  {{{{m}}+{{one}}}}}})}}}}\unicdbdjdcd{{{{one}} \in {{Npos}}}}\unicdbdjdcd\\
{{({{\unicdcdadad m \in {{Npos}} .  {{{{{{m}}+{{one}}}}\unicdcdgdad{{one}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad m \in {{Npos}} .  {{\unicdcdadad q : {{{{\iota}}\unicdbdjdcd{{o}}}} .  {{{{{{q}}~{{one}}}}\unicdbdjdcd{{{{({{\unicdcdadad n \in {{Npos}} .  {{{{q}}~{{({{{{n}}+{{one}}}})}}}}}})}}\unicdbdjdcd{{{{q}}~{{m}}}}}}}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad n m \in {{Npos}} .  {{{{{{{{{{{{{{\mname{{explicit\_Nats\_one\_plus}}}}~{{Npos}}}}~{{one}}}}~{{({{\uniddcgcg m .  {{{{m}}+{{one}}}}}})}}}}~{{n}}}}~{{m}}}}={{{{n}}+{{m}}}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad n m \in {{Npos}} .  {{{{{{{{{{{{{{\mname{{explicit\_Nats\_one\_mult}}}}~{{Npos}}}}~{{one}}}}~{{({{\uniddcgcg m .  {{{{m}}+{{one}}}}}})}}}}~{{n}}}}~{{m}}}}={{{{n}}*{{m}}}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad n m \in {{Npos}} .  {{{{{{n}}+{{m}}}} \in {{Npos}}}}}})}}\unicdbdjdcd\\
{{{{({{\unicdcdadad n m \in {{Npos}} .  {{{{{{n}}*{{m}}}} \in {{Npos}}}}}})}}\unicdbdjdcd{{p}}}})\\
{\unicdbdjdcd}{p}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 70d4a40bcc65e646c44adc246e6e8230f11d26380216c98eef3ce0f533c5b967 \\
Pure Prop Address: & TMWVNiuNPNFnodbziNN8nLxyxLMnKWrd8wJ \\
Theory Prop Id: & ccf61651d2adec6894aedbbc427dceb7844e2399f21269514640c7e6094ad427 \\
Theory Prop Address: & TMFByiQaDpiDUkPeJbt5Bp3Vmn1hJbuuYP1
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_OrderedField_Z_props
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfpechegfgchfgeggejgfgmgegpfkfpfahchpgahdh} 
$$
\begin{array}{c}
{{{\mname{{explicit\_OrderedField}}}}}{\unicdbdjdcd}{\unicdcdadad p : }{{{o}}}{ .  }\\
({{({{\unicdcdadad n \in {{Npos}} .  {{{{\prenc{{n}}}} \in {{Z}}}}}})}}\unicdbdjdcd\\
{{{{zero}} \in {{Z}}}}\unicdbdjdcd{{{{Npos}} \subseteq {{Z}}}}\unicdbdjdcd{{{{Z}} \subseteq {{R}}}}\unicdbdjdcd\\
{{({{\unicdcdadad n \in {{Z}} .  {{\unicdcdadad q : {{o}} .  {{{{({{{{{{\prenc{{n}}}} \in {{Npos}}}}\unicdbdjdcd{{q}}}})}}\unicdbdjdcd{{{{({{{{{{n}}={{zero}}}}\unicdbdjdcd{{q}}}})}}\unicdbdjdcd{{{{({{{{{{n}} \in {{Npos}}}}\unicdbdjdcd{{q}}}})}}\unicdbdjdcd{{q}}}}}}}}}}}})}}\unicdbdjdcd\\
{{{{one}} \in {{Z}}}}\unicdbdjdcd{{{{\prenc{{one}}}} \in {{Z}}}}\unicdbdjdcd\\
{{({{\unicdcdadad m \in {{Z}} .  {{{{\prenc{{m}}}} \in {{Z}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad n m \in {{Z}} .  {{{{{{n}}+{{m}}}} \in {{Z}}}}}})}}\unicdbdjdcd\\
{{{{({{\unicdcdadad n m \in {{Z}} .  {{{{{{n}}*{{m}}}} \in {{Z}}}}}})}}\unicdbdjdcd{{p}}}})\\
{\unicdbdjdcd}{p}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & c4e83c38fecfc73fc1d09e7d004296072c59b1e4f2df931d758d29e6794ea856 \\
Pure Prop Address: & TMXcg17hazxWWPbWnFd6LixgqsqD72qWt13 \\
Theory Prop Id: & 5d739c339801f054de73227f43deae05f5146a6f72e3301a34806a65741eee8f \\
Theory Prop Address: & TMdyXYYsofQoayXp7LxqNscqFCZMBXVaVYV
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_OrderedField_Q_props
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfpechegfgchfgeggejgfgmgegpfbfpfahchpgahdh} 
$$
\begin{array}{c}
{{{\mname{{explicit\_OrderedField}}}}}{\unicdbdjdcd}{\unicdcdadad p : }{{{o}}}{ .  }\\
({{{{Q}} \subseteq {{R}}}}\unicdbdjdcd\\
{{({{\unicdcdadad x \in {{Q}} .  {{\unicdcdadad q : {{o}} .  {{{{({{{{{{x}} \in {{R}}}}\unicdbdjdcd{{\unicdcdadad n \in {{Z}} .  {{\unicdcdadad m \in {{Npos}} .  {{{{{{{{m}}*{{x}}}}={{n}}}}\unicdbdjdcd{{q}}}}}}}}}})}}\unicdbdjdcd{{q}}}}}}}})}}\unicdbdjdcd\\
{{({{\unicdcdadad x \in {{R}} .  {{\unicdcdadad n \in {{Z}} .  {{\unicdcdadad m \in {{Npos}} .  {{{{{{{{m}}*{{x}}}}={{n}}}}\unicdbdjdcd{{{{x}} \in {{Q}}}}}}}}}}}})}}\unicdbdjdcd{{p}})\\
{\unicdbdjdcd}{p}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 469ebe93febae512d65ef077bb259d3d61a42e332d5dc0f218b4ef51c641e3e4 \\
Pure Prop Address: & TMTZyHSuTABLn2UE5U2gcU2Ezo5LNbr4p3D \\
Theory Prop Id: & d268c341664267b91610963ba224b4a1a9c0f9f442a16df66f09d45352a4151a \\
Theory Prop Address: & TMds236CmEKbqpnTaTJdR2MqiniGBAQsAPi
\end{tabular}
\end{center}

\end{theorem}
\begin{definition}\label{def:fgihahmgjgdgjgehpfcffgbgmgdh}
$\mname{explicit\_Reals}$ is the opaque object of type ${o}$ identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Object Id: & 2c81615a11c9e3e301f3301ec7862ba122acea20bfe1c120f7bdaf5a2e18faf4 \\
Pure Object Address: & TMNQkXLgjhMYMywv7BnJ8Buh3QQLNR7YL5B \\
Theory Object Id: & f814a2e6f2e99b382ad540cb48300cde1d9995f4b6b2b5af7856369fd2644732 \\
Theory Object Address: & TMRfnwEvCdNWYa7FnDpZ9E82K56Dx1FvxWm
\end{tabular}
\end{center}

\end{definition}
\begin{verbatim}
explicit_Reals_I
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcffgbgmgdhpfje} 
$$
\begin{array}{c}
  {{{\mname{{explicit\_OrderedField}}}}}{\unicdbdjdcd}\\
  {{{({{\unicdcdadad x y \in {{R}} .  {{{{{{zero}}<{{x}}}}\unicdbdjdcd{{{{{{zero}}\unicdcdgded{{y}}}}\unicdbdjdcd{{\unicdcdaddd n \in {{N}} .  {{{{y}}\unicdcdgded{{{{n}}*{{x}}}}}}}}}}}}}})}}}{\unicdbdjdcd}\\
(\unicdcdadad a b \in {{{{R}}^{{N}}}} .  {{({{\unicdcdadad n \in {{N}} .  {{{{{{{{{{a}}~{{n}}}}\unicdcdgded{{{{b}}~{{n}}}}}}\unicdcdcdhd{{{{{{a}}~{{n}}}}\unicdcdgded{{{{a}}~{{({{{{n}}+{{one}}}})}}}}}}}}\unicdcdcdhd{{{{{{b}}~{{({{{{n}}+{{one}}}})}}}}\unicdcdgded{{{{b}}~{{n}}}}}}}}}})}}\unicdbdjdcd\\
{{\unicdcdaddd x \in {{R}} .  {{\unicdcdadad n \in {{N}} .  {{{{{{{{a}}~{{n}}}}\unicdcdgded{{x}}}}\unicdcdcdhd{{{{x}}\unicdcdgded{{{{b}}~{{n}}}}}}}}}}}})\\
{\unicdbdjdcd}{{\mname{{explicit\_Reals}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 409e2333061c2a93e2645163cc79fc5d5af155c8a5d27793194dc767da89abbb \\
Pure Prop Address: & TMV9L8eBVS4dZTimiRu7xTnjDG7k6PkcS8x \\
Theory Prop Id: & 5c0c700ed594f122d6868607cbbbb42d933731fe7421678006f15345427a750c \\
Theory Prop Address: & TMFrB18DrFskuCZs1RC1v2N6mv4m2xbxyyh
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Reals_E
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcffgbgmgdhpffe} 
$$
\begin{array}{c}
{\unicdcdadad q : }{{{o}}}{ .  }\\
({{\mname{{explicit\_Reals}}}}\unicdbdjdcd{{\mname{{explicit\_OrderedField}}}}\unicdbdjdcd\\
{{({{\unicdcdadad x y \in {{R}} .  {{{{{{zero}}<{{x}}}}\unicdbdjdcd{{{{{{zero}}\unicdcdgded{{y}}}}\unicdbdjdcd{{\unicdcdaddd n \in {{N}} .  {{{{y}}\unicdcdgded{{{{n}}*{{x}}}}}}}}}}}}}})}}\unicdbdjdcd\\
(\unicdcdadad a b \in {{{{R}}^{{N}}}} . {{({{\unicdcdadad n \in {{N}} .  {{{{{{{{{{a}}~{{n}}}}\unicdcdgded{{{{b}}~{{n}}}}}}\unicdcdcdhd{{{{{{a}}~{{n}}}}\unicdcdgded{{{{a}}~{{({{{{n}}+{{one}}}})}}}}}}}}\unicdcdcdhd{{{{{{b}}~{{({{{{n}}+{{one}}}})}}}}\unicdcdgded{{{{b}}~{{n}}}}}}}}}})}}\unicdbdjdcd\\
{{\unicdcdaddd x \in {{R}} .  {{\unicdcdadad n \in {{N}} .  {{{{{{{{a}}~{{n}}}}\unicdcdgded{{x}}}}\unicdcdcdhd{{{{x}}\unicdcdgded{{{{b}}~{{n}}}}}}}}}}}})\\
\unicdbdjdcd{{q}})\\
{\unicdbdjdcd}{{{\mname{{explicit\_Reals}}}}}{\unicdbdjdcd}{q}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 21d90e2433a10558f7145bc3be6f01fa8745c28bffc25ad66bd1a18358b3b240 \\
Pure Prop Address: & TMGdZwHMdLeLHxRbHQCHJtCbKDNcLtG3W8L \\
Theory Prop Id: & 4da66ca8d1ae9ed2c059a4f5bc10b24ce6225436b72100092ed91505c18552ff \\
Theory Prop Address: & TMXm1gKZKK9VncpZdpgFvZ65WUBmGNKHtic
\end{tabular}
\end{center}

\end{theorem}
\begin{verbatim}
explicit_Reals_characteristic_0
\end{verbatim}
\begin{theorem}\label{thm:fgihahmgjgdgjgehpfcffgbgmgdhpfdgigbgchbgdgehfgchjgdhehjgdgpfad} 
$$
\begin{array}{c}
{{{\mname{{explicit\_Reals}}}}}{\unicdbdjdcd}{\unicdcdadad n \in }{{{\mname{{omega}}}}}{ .  }
{{{{{{{{{{\mname{{nat\_primrec}}}}~{{one}}}}~{{({{\uniddcgcg \_ r .  {{{{{{plus}}~{{one}}}}~{{r}}}}}})}}}}~{{n}}}}\unicdcdgdad{{zero}}}}.
\end{array}
$$
 The proposition is identified by the following information:
\begin{center}
\scriptsize
\begin{tabular}{rl}
Pure Prop Id: & 0212c2930b33db49e6a4620cb445fdddf720a725cafcc5cdfd73aba5653545a7 \\
Pure Prop Address: & TMQD99B4xAaxuUtBVEmerL9nB3AVPpeVrb5 \\
Theory Prop Id: & a77c5ab95a85405cab2dc8eb8cf6de3db3512e2461a8c18fdbf2c5586157d584 \\
Theory Prop Address: & TMcXpA2UzrnRUBX4icewcaFFnK1yHVkVbAY
\end{tabular}
\end{center}

\end{theorem}
