\import Algebra.Meta
\import Algebra.Monoid
\import Arith.Real
\import Arith.Real.Field
\import Function.Meta
\import Logic
\import Topology.MetricSpace
\import Topology.NormedAbGroup.Real
\import Topology.TopRing

\instance RealNearField : NearField Real
  | CRing => RealField
  | TopAbGroup => RealNormed
  | *-cont => RealField.*-cover
  | inv-dense {x} Uo Ux => \case (dist_open {RealNormed}). Uo Ux \with {
    | inP (eps,eps>0,h) =>
      \have t => rat_real_<. eps>0
      \in \case real-located {} {x} {x + RealField.half eps} linarith \with {
        | byLeft x<0 => inP (x, RealField.neg#0 x<0, Ux)
        | byRight p => inP (x + RealField.half eps, RealField.pos#0 p, h $ real_<_U. $ RealAbGroup.abs_-_< linarith linarith)
      }
  }