Real

\import Algebra.Field
\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ordered
\import Algebra.Semiring
\import Arith.Int
\import Arith.Rat
\import Data.Or
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\open LinearOrder \hiding (<=)

\record LowerReal (L : Rat -> \Prop) {
  | L-inh : ∃ L
  | L-closed {q q' : Rat} : L q -> q' < q -> L q'
  | L-rounded {q : Rat} : L q -> ∃ (r : L) (q < r)

  \lemma L_<= {q r : Rat} (Lq : L q) (p : r <= q) : L r
    => \case <=-dec p \with {
      | inl r<q => L-closed Lq r<q
      | inr r=q => transportInv L r=q Lq
    }
}

\instance LowerRealAbMonoid : AbMonoid LowerReal
  | zro => Real.fromRat 0
  | + => +
  | zro-left => (\peval _ + _) *> exts \lam a => ext (\lam (inP (b,b<0,c,c<x,a<b+c)) => L-closed c<x linarith, \lam a<x => \case L-rounded a<x \with {
      | inP (b,b<x,a<b) => inP ((a - b) * ratio 1 2, linarith, b, b<x, linarith)
    })
  | +-assoc => exts (\lam a => ext (\lam r => \case +_L.1 r \with {
      | inP (b, r', c, c<z,a<b+c) => \case +_L.1 r' \with {
        | inP (d,d<x,e,e<y,b<d+e) => +_L.2 $ inP (d, d<x, (a - d RatField.+ c RatField.+ e) * ratio 1 2, +_L.2 $ inP (e, e<y, c, c<z, linarith), linarith)
      }
    }, \lam r => \case +_L.1 r \with {
      | inP (b, b<x, c, r', a<b+c) => \case +_L.1 r' \with {
        | inP (d,d<y,e,e<z,c<d+e) => +_L.2 $ inP ((a - e RatField.+ b RatField.+ d) * ratio 1 2, +_L.2 $ inP (b, b<x, d, d<y, linarith), e, e<z, linarith)
      }
    }))
  | +-comm => exts (\lam a => ext (\lam r => \case +_L.1 r \with {
      | inP (b,b<x,c,c<y,a<b+c) => +_L.2 $ inP $ later (c, c<y, b, b<x, rewrite RatField.+-comm a<b+c)
    }, \lam r => \case +_L.1 r \with {
      | inP (c,c<y,b,b<x,a<c+b) => +_L.2 $ inP $ later (b, b<x, c, c<y, rewrite RatField.+-comm a<c+b)
    }))
  \where {
    \sfunc \infixl 6 + (x y : LowerReal) : LowerReal \cowith
      | L a => ∃ (b : x.L) (c : y.L) (a < b RatField.+ c)
      | L-inh => \case x.L-inh, y.L-inh \with {
        | inP (a,a<x), inP (b,b<y) => inP (a RatField.+ b - 1, inP (a, a<x, b, b<y, linarith))
      }
      | L-closed (inP (a,a<x,b,b<y,q<a+b)) q'<q => inP (a, a<x, b, b<y, q'<q <∘ q<a+b)
      | L-rounded {q} (inP (a,a<x,b,b<y,q<a+b)) => inP (RatField.mid q (a RatField.+ b), inP (a, a<x, b, b<y, RatField.mid<right q<a+b), RatField.mid>left q<a+b)

    \lemma +_L {x y : LowerReal} {a : Rat} : Real.L {x + y} a <-> ∃ (b : x.L) (c : y.L) (a < b RatField.+ c)
      => rewrite (\peval x + y) <->refl

    \lemma +-rat {x y : Rat} : Real.fromRat x + Real.fromRat y = {LowerReal} Real.fromRat (x RatField.+ y)
      => (\peval _ + _) *> {LowerReal} exts \lam a => ext (\lam (inP (b,b<x,c,c<y,a<b+c)) => a<b+c <∘ OrderedAddMonoid.<_+ b<x c<y,
            \lam a<x+y => inP (x - (x RatField.+ y - a) * ratio 1 3, linarith, y - (x RatField.+ y - a) * ratio 1 3, linarith, linarith))
  }

\instance LowerRealLattice : Lattice LowerReal
  | <= (x y : LowerReal) => ∀ {a : x.L} (y.L a)
  | <=-refl a<x => a<x
  | <=-transitive p q a<x => q (p a<x)
  | <=-antisymmetric p q => exts \lam a => ext (p,q)
  | meet => meet
  | meet-left s => (meet_L.1 s).1
  | meet-right s => (meet_L.1 s).2
  | meet-univ z<=x z<=y a<z => meet_L.2 (z<=x a<z, z<=y a<z)
  | join => join
  | join-left a<x => join_L.2 (byLeft a<x)
  | join-right a<y => join_L.2 (byRight a<y)
  | join-univ x<=z y<=z r => \case join_L.1 r \with {
    | byLeft a<x => x<=z a<x
    | byRight a<y => y<=z a<y
  }
  \where {
    \sfunc meet (x y : LowerReal) : LowerReal \cowith
      | L a => \Sigma (x.L a) (y.L a)
      | L-inh => \case x.L-inh, y.L-inh \with {
        | inP (a,a<x), inP (b,b<y) => inP (a ∧ b, (x.L_<= a<x meet-left, y.L_<= b<y meet-right))
      }
      | L-closed (q<x,q<y) q'<q => (x.L-closed q<x q'<q, y.L-closed q<y q'<q)
      | L-rounded (q<x,q<y) => \case x.L-rounded q<x, y.L-rounded q<y \with {
        | inP (r,r<x,q<r), inP (r',r'<y,q<r') => inP (r ∧ r', (x.L_<= r<x meet-left, y.L_<= r'<y meet-right), <_meet-univ q<r q<r')
      }

    \lemma meet_L {x y : LowerReal} {a : Rat} : Real.L {meet x y} a <-> (\Sigma (x.L a) (y.L a))
      => rewrite (\peval meet x y) <->refl

    \sfunc join (x y : LowerReal) : LowerReal \cowith
      | L a => x.L a || y.L a
      | L-inh => \case x.L-inh \with {
        | inP (a,a<x) => inP (a, byLeft a<x)
      }
      | L-closed e q'<q => ||.map (x.L-closed __ q'<q) (y.L-closed __ q'<q) e
      | L-rounded => \case \elim __ \with {
        | byLeft q<x => \case x.L-rounded q<x \with {
          | inP (r,r<x,q<r) => inP (r, byLeft r<x, q<r)
        }
        | byRight q<y => \case y.L-rounded q<y \with {
          | inP (r,r<y,q<r) => inP (r, byRight r<y, q<r)
        }
      }

    \lemma join_L {x y : LowerReal} {a : Rat} : Real.L {join x y} a <-> x.L a || y.L a
      => rewrite (\peval join x y) <->refl
  }

\record UpperReal (U : Rat -> \Prop) {
  | U-inh : ∃ U
  | U-closed {q q' : Rat} : U q -> q < q' -> U q'
  | U-rounded {q : Rat} : U q -> ∃ (r : U) (r < q)

  \lemma U_<= {q r : Rat} (Uq : U q) (p : q <= r) : U r
    => \case <=-dec p \with {
      | inl q<r => U-closed Uq q<r
      | inr q=r => transport U q=r Uq
    }

  \lemma natBounded : ∃ (n : Nat) (U n)
    => \case U-inh \with {
      | inP (a,Ua) => inP (iabs $ rat_ceiling a, U_<= Ua $ rat_ceiling>id <=∘ later (rewrite iabs=abs $ fromInt_<= LinearlyOrderedAbGroup.abs>=id))
    }
}

\instance UpperRealAbMonoid : AbMonoid UpperReal
  | zro => Real.fromRat 0
  | + => +
  | zro-left => (\peval _ + _) *> exts \lam a => ext (\lam (inP (b,b<0,c,c<x,a<b+c)) => U-closed c<x linarith, \lam a<x => \case U-rounded a<x \with {
    | inP (b,b<x,a<b) => inP ((a - b) * ratio 1 2, linarith, b, b<x, linarith)
  })
  | +-assoc => exts \lam a => ext (\lam r => \case +_U.1 r \with {
    | inP (b, r', c, c<z,a<b+c) => \case +_U.1 r' \with {
      | inP (d,d<x,e,e<y,b<d+e) => +_U.2 $ inP (d, d<x, (a - d RatField.+ c RatField.+ e) * ratio 1 2, +_U.2 $ inP (e, e<y, c, c<z, linarith), linarith)
    }
  }, \lam r => \case +_U.1 r \with {
    | inP (b, b<x, c, r', a<b+c) => \case +_U.1 r' \with {
      | inP (d,d<y,e,e<z,c<d+e) => +_U.2 $ inP ((a - e RatField.+ b RatField.+ d) * ratio 1 2, +_U.2 $ inP (b, b<x, d, d<y, linarith), e, e<z, linarith)
    }
  })
  | +-comm => exts \lam a => ext (\lam r => \case +_U.1 r \with {
    | inP (b,b<x,c,c<y,a<b+c) => +_U.2 $ inP $ later (c, c<y, b, b<x, rewrite RatField.+-comm a<b+c)
  }, \lam r => \case +_U.1 r \with {
    | inP (c,c<y,b,b<x,a<c+b) => +_U.2 $ inP $ later (b, b<x, c, c<y, rewrite RatField.+-comm a<c+b)
  })
  \where {
    \sfunc \infixl 6 + (x y : UpperReal) : UpperReal \cowith
      | U a => ∃ (b : x.U) (c : y.U) (b RatField.+ c < a)
      | U-inh => \case x.U-inh, y.U-inh \with {
        | inP (a,x<a), inP (b,y<b) => inP (a RatField.+ b RatField.+ 1, inP (a, x<a, b, y<b, linarith))
      }
      | U-closed (inP (a,a<x,b,b<y,a+b<q)) q<q' => inP (a, a<x, b, b<y, a+b<q <∘ q<q')
      | U-rounded {q} (inP (a,a<x,b,b<y,a+b<q)) => inP (RatField.mid (a RatField.+ b) q, inP (a, a<x, b, b<y, RatField.mid>left a+b<q), RatField.mid<right a+b<q)

    \lemma +_U {x y : UpperReal} {a : Rat} : Real.U {x + y} a <-> ∃ (b : x.U) (c : y.U) (b RatField.+ c < a)
      => rewrite (\peval x + y) <->refl

    \lemma +-rat {x y : Rat} : Real.fromRat x + Real.fromRat y = {UpperReal} Real.fromRat (x RatField.+ y)
      => (\peval _ + _) *> {UpperReal} exts \lam a => ext (\lam (inP (b,x<b,c,y<c,b+c<a)) => OrderedAddMonoid.<_+ x<b y<c <∘ b+c<a,
            \lam a<x+y => inP (x - (x RatField.+ y - a) * ratio 1 3, linarith, y - (x RatField.+ y - a) * ratio 1 3, linarith, linarith))
  }

\instance UpperRealLattice : Lattice UpperReal
  | <= (x y : UpperReal) => ∀ {a : y.U} (x.U a)
  | <=-refl x<a => x<a
  | <=-transitive p q x<a => p (q x<a)
  | <=-antisymmetric p q => exts \lam a => ext (q,p)
  | meet => meet
  | meet-left x<a => meet_U.2 (byLeft x<a)
  | meet-right y<a => meet_U.2 (byRight y<a)
  | meet-univ x<=z y<=z r => \case meet_U.1 r \with {
    | byLeft a<x => x<=z a<x
    | byRight a<y => y<=z a<y
  }
  | join => join
  | join-left s => (join_U.1 s).1
  | join-right s => (join_U.1 s).2
  | join-univ z<=x z<=y a<z => join_U.2 (z<=x a<z, z<=y a<z)
  \where {
    \sfunc meet (x y : UpperReal) : UpperReal \cowith
      | U a => x.U a || y.U a
      | U-inh => \case x.U-inh \with {
        | inP (a,x<a) => inP (a, byLeft x<a)
      }
      | U-closed e q'<q => ||.map (x.U-closed __ q'<q) (y.U-closed __ q'<q) e
      | U-rounded => \case \elim __ \with {
        | byLeft q<x => \case x.U-rounded q<x \with {
          | inP (r,r<x,q<r) => inP (r, byLeft r<x, q<r)
        }
        | byRight q<y => \case y.U-rounded q<y \with {
          | inP (r,r<y,q<r) => inP (r, byRight r<y, q<r)
        }
      }

    \lemma meet_U {x y : UpperReal} {a : Rat} : Real.U {meet x y} a <-> x.U a || y.U a
      => rewrite (\peval meet x y) <->refl

    \sfunc join (x y : UpperReal) : UpperReal \cowith
      | U a => \Sigma (x.U a) (y.U a)
      | U-inh => \case x.U-inh, y.U-inh \with {
        | inP (a,a<x), inP (b,b<y) => inP (a ∨ b, (x.U_<= a<x join-left, y.U_<= b<y join-right))
      }
      | U-closed (q<x,q<y) q'<q => (x.U-closed q<x q'<q, y.U-closed q<y q'<q)
      | U-rounded (q<x,q<y) => \case x.U-rounded q<x, y.U-rounded q<y \with {
        | inP (r,r<x,q<r), inP (r',r'<y,q<r') => inP (r ∨ r', (x.U_<= r<x join-left, y.U_<= r'<y join-right), <_join-univ q<r q<r')
      }

    \lemma join_U {x y : UpperReal} {a : Rat} : Real.U {join x y} a <-> (\Sigma (x.U a) (y.U a))
      => rewrite (\peval join x y) <->refl
  }

\func \infix 4 <LU (x : UpperReal) (y : LowerReal) : \Prop
  => ∃ (a : Rat) (x.U a) (y.L a)

\func \infix 4 <=L (x y : LowerReal) : \Prop
  => \Pi {a : Rat} -> x.L a -> y.L a

\lemma <LU-transitive {x : UpperReal} {y z : LowerReal} (p : x <LU y) (q : y <=L z) : x <LU z \elim p
  | inP (a,x<a,a<y) => inP (a, x<a, q a<y)

\record Real \extends LowerReal, UpperReal {
  | LU-disjoint {q : Rat} : L q -> U q -> Empty
  | LU-located {q r : Rat} : q < r -> L q || U r
  | LU-focus (eps : Rat) : eps > 0 -> ∃ (a : L) (U (a + eps))

  \default LU-located {q} {r} q<r => \case LU-focus (r - q) (RatField.pos_>0 q<r) \with {
    | inP (s,Ls,Us+r-q) => \case trichotomy q s \with {
      | less q<s => byLeft (L-closed Ls q<s)
      | equals q=s => byLeft (transportInv L q=s Ls)
      | greater s<q => byRight $ U-closed Us+r-q $ transport (_ <) (equation : q + (r - q) = r) (<_+-left (r - q) s<q)
    }
  }

  \default L-inh => TruncP.map (LU-focus 1 idp) (\lam x => (x.1,x.2))

  \default U-inh => TruncP.map (LU-focus 1 idp) (\lam x => (x.1 + 1, x.3))

  \default LU-focus \as LU-focus-impl (eps : Rat) (eps>0 : eps > 0) : ∃ (a : L) (U (a + eps)) => \case L-inh, U-inh \with {
    | inP (q,Lq), inP (r,Ur) =>
      \let | m r q => (r - q) * finv 3
           | LU-less {q} {r} (Lq : L q) (Ur : U r) : q < r => \case dec<_<= q r \with {
             | inl q<r => q<r
             | inr r<=q => absurd $ LU-disjoint Lq (U_<= Ur r<=q)
           }
      \in \case focus-iter (ratio 3 2) rat_<=-dec (\lam q r => \Sigma (L q) (U r)) (\lam q r (Lq,Ur) => \case LU-located (linarith (usingOnly (LU-less Lq Ur))) \with {
        | byLeft Lq+m => inP (q + m r q, r, (Lq+m,Ur), linarith)
        | byRight Ur-m => inP (q, r - m r q, (Lq,Ur-m), linarith)
      }) (iabs $ rat_ceiling $ finv eps * (r - q)) q r (Lq,Ur) \with {
        | inP (q',r',(Lq',Ur'),p) => inP (q', Lq', U-closed Ur'
          \have | r-q>0 {q} {r} (Lq : L q) (Ur : U r) : 0 < r - q => linarith (usingOnly (LU-less Lq Ur))
                | pr>0 => RatField.<_*_positive_positive (finv>0 eps>0) (r-q>0 Lq Ur)
                | c>0 => fromInt_<.conv $ pr>0 <∘l rat_ceiling>id
                | s : (r' - q') * (finv eps * (r - q)) < r - q
                    => <_*_positive-right (r-q>0 Lq' Ur') (rat_ceiling>id <∘r fromInt_<= (Preorder.=_<= $ inv $ iabs.ofPos $ <_<= c>0) <∘r pow>id _) <∘l p
                | t => transport (_ <) (pmap (_ *) finv_* *> inv *-assoc *> pmap (`* _) (finv-right $ RatField.>_/= $ r-q>0 Lq Ur) *> ide-left *> finv_finv) (<_rotate-right pr>0 s)
          \in linarith (usingOnly t))
      }
  }

  \lemma LU-less {q r : Rat} (Lq : L q) (Ur : U r) : q < r
    => \case dec<_<= q r \with {
      | inl q<r => q<r
      | inr r<=q => absurd $ LU-disjoint Lq (U_<= Ur r<=q)
    }

  \lemma LU_*-focus-right (x>0 : L 0) {d : Rat} (d>1 : 1 < d) : ∃ (a : Rat) (0 < a) (L a) (U (a * d))
    => \case L-rounded x>0 \with {
      | inP (a0,a0<x,a0>0) => \case LU-focus (a0 * (d - 1)) (OrderedSemiring.<_*_positive_positive a0>0 linarith) \with {
        | inP (a,a<x,p) => inP (a0 ∨ a, a0>0 <∘l join-left, real_join_L a0<x a<x, U_<= p $ later $ rewrite {2} (linarith : d = 1 + (d - 1), ldistr) $ rewrite ide-right $ LinearlyOrderedAbMonoid.<=_+ join-right $ <=_*_positive-left join-left linarith)
      }
    }

  \lemma LU_*-focus-left (x>0 : L 0) {c : Rat} (c<1 : c < 1) : ∃ (b : Rat) (L (b * c)) (U b)
    => \case dec<_<= 0 c \with {
      | inl c>0 => \case LU_*-focus-right x>0 {finv c} (finv>1 c>0 c<1) \with {
        | inP (a,_,a<x,x<ac1) => inP (a * finv c, transportInv L (*-assoc *> pmap (a *) (finv-left $ RatField.>_/= c>0) *> ide-right) a<x, x<ac1)
      }
      | inr c<=0 => \case U-inh \with {
        | inP (b,x<b) => inP (b, L_<= x>0 $ <=_*_positive_negative (<_<= $ LU-less x>0 x<b) c<=0, x<b)
      }
    }
} \where {
  \open DiscreteOrderedField
  \open DiscreteField
  \open LinearlyOrderedSemiring

  \func focus-iter (rat : Rat) (rat>=0 : 0 <= rat) (P : Rat -> Rat -> \Prop) (f : \Pi (q r : Rat) -> P q r -> ∃ (q' r' : P) ((r' - q') * rat <= r - q)) (n : Nat) (q r : Rat) (Pqr : P q r) : ∃ (q' r' : P) ((r' - q') * Monoid.pow rat n <= r - q) \elim n
    | 0 => inP (q, r, Pqr, transportInv (`<= _) ide-right <=-refl)
    | suc n => \case f q r Pqr \with {
      | inP (q',r',Pq'r',c) => \case focus-iter rat rat>=0 P f n q' r' Pq'r' \with {
        | inP (q'',r'',Pq''r'',d) => inP (q'', r'', Pq''r'', Preorder.=_<= (inv *-assoc) <=∘ RatField.<=_*_positive-left d rat>=0 <=∘ c)
      }
    }

  \lemma pow>id (n : Nat) : Monoid.pow (ratio 3 2) n > n \elim n
    | 0 => idp
    | 1 => idp
    | 2 => idp
    | suc (suc (suc n)) => linarith <∘r <_*_positive-left (pow>id (suc (suc n))) idp

  \use \coerce fromRat (x : Rat) : Real \cowith
    | L => `< x
    | L-closed s t => t <∘ s
    | L-rounded q<x => TruncP.map (isDense q<x) (\lam t => (t.1,t.3,t.2))
    | U => x <
    | U-closed => <∘
    | U-rounded => isDense
    | LU-disjoint q<x x<q => <-irreflexive (q<x <∘ x<q)
    | LU-focus eps eps>0 => inP (x - eps * finv 2, linarith, linarith)

  \lemma real-ext {x y : Real} (p : \Pi {a b : Rat} -> (\Sigma (x.L a) (x.U b)) <-> (\Sigma (y.L a) (y.U b))) : x = y
    => \case x.L-inh, x.U-inh, y.L-inh, y.U-inh \with {
      | inP (x1,x1<x), inP (x2,x<x2), inP (y1,y1<y), inP (y2,y<y2) =>
          ext (ext \lam z => ext (\lam z<x => (p.1 (z<x,x<x2)).1, \lam z<y => (p.2 (z<y,y<y2)).1),
               ext \lam z => ext (\lam x<z => (p.1 (x1<x,x<z)).2, \lam y<z => (p.2 (y1<y,y<z)).2))
    }

  \lemma real-lu-ext {x y : Real} (p : x = {LowerReal} y) (q : x = {UpperReal} y) : x = y
    => ext (pmap (\lam (z : LowerReal) => z.L) p, pmap (\lam (z : UpperReal) => z.U) q)

  \lemma fromRat-inj {x y : Rat} (p : fromRat x = fromRat y) : x = y
    => <=-antisymmetric (rat_real_<=.2 $ RealAbGroup.=_<= p) (rat_real_<=.2 $ RealAbGroup.=_<= $ inv p)
}

\instance RealAbGroup : LinearlyOrderedAbGroup Real
  | zro => Real.fromRat 0
  | + => +
  | zro-left => (\peval _ + _) *> Real.real-lu-ext zro-left zro-left
  | +-comm => (\peval _ + _) *> Real.real-lu-ext (later +-comm) (later +-comm) *> inv (\peval _ + _)
  | +-assoc => Real.real-lu-ext (+_L.lower *> {LowerReal} pmap {LowerReal} (LowerRealAbMonoid.`+ _) +_L.lower *> {LowerReal} LowerRealAbMonoid.+-assoc *> {LowerReal} pmap (_ LowerRealAbMonoid.+) (inv {LowerReal} +_L.lower) *> {LowerReal} inv {LowerReal} +_L.lower)
                                (+_U.upper *> {UpperReal} pmap {UpperReal} (UpperRealAbMonoid.`+ _) +_U.upper *> {UpperReal} UpperRealAbMonoid.+-assoc *> {UpperReal} pmap (_ UpperRealAbMonoid.+) (inv {UpperReal} +_U.upper) *> {UpperReal} inv {UpperReal} +_U.upper)
  | negative => negative
  | negative-left {x : Real} => exts (
      \lam a => ext (\lam r => \case +_L.1 r \with {
        | inP (b,x<-b,c,c<x,a<b+c) => a<b+c <∘ linarith (x.LU-less c<x $ negative_L.1 x<-b)
      }, \lam a<0 => \case x.LU-focus (a * ratio -1 2) linarith \with {
        | inP (b,b<x,x<b-a/2) => +_L.2 $ inP (RatField.negative (b RatField.+ a * ratio -1 2), negative_L.2 $ simplify x<b-a/2, b, b<x, linarith)
      }),
      \lam a => ext (\lam r => \case +_U.1 r \with {
        | inP (b,-b<x,c,x<c,b+c<a) => linarith (x.LU-less (negative_U.1 -b<x) x<c) <∘ b+c<a
      }, \lam a>0 => \case x.LU-focus (a * ratio 1 2) linarith \with {
        | inP (b,b<x,x<b+a/2) => +_U.2 $ inP (RatField.negative b, negative_U.2 $ simplify b<x, _, x<b+a/2, linarith)
      }))
  | isPos (x : Real) => x.L 0
  | zro/>0 => \case __
  | positive_+ x>0 y>0 => \case L-rounded x>0 \with {
    | inP (a,a<x,a>0) => +_L.2 $ inP (a, a<x, 0, y>0, simplify a>0)
  }
  | <_+-comparison x y r => \case +_L.1 r \with {
    | inP (b,b<x,c,c<y,b+c>0) => \case dec<_<= 0 b \with {
      | inl b>0 => byLeft (L-closed b<x b>0)
      | inr b<=0 => byRight (L-closed c<y linarith)
    }
  }
  | <_+-connectedness p q => exts (\lam a => ext (\lam a<x => \case dec<_<= a 0 \with {
    | inl a<0 => a<0
    | inr a>=0 => absurd $ p $ LowerReal.L_<= a<x a>=0
  }, \lam a<0 => \case LU-located a<0 \with {
    | byLeft a<x => a<x
    | byRight x<0 => absurd $ q $ negative_L.2 x<0
  }), \lam a => ext (\lam x<a => \case dec<_<= 0 a \with {
    | inl a>0 => a>0
    | inr a<=0 => absurd $ q $ negative_L.2 $ UpperReal.U_<= x<a a<=0
  }, \lam a>0 => \case LU-located a>0 \with {
    | byLeft x>0 => absurd $ p x>0
    | byRight x<a => x<a
  }))
  | meet => meet
  | meet-left r => \case +_L.1 r \with {
    | inP (b,s,c,x<-c,b+c>0) => <-irreflexive $ Real.LU-less (meet_L.1 s).1 (U-closed (negative_L.1 x<-c) linarith)
  }
  | meet-right r => \case +_L.1 r \with {
    | inP (_,s,c,y<-c,b+c>0) => <-irreflexive $ Real.LU-less (meet_L.1 s).2 (U-closed (negative_L.1 y<-c) linarith)
  }
  | meet-univ z<=x z<=y r => \case +_L.1 r \with {
    | inP (b, b<z, c, r, b+c>0) => \case meet_U.1 $ negative_L.1 r \with {
      | byLeft x<-c => z<=x $ +_L.2 $ inP (b, b<z, c, negative_L.2 x<-c, b+c>0)
      | byRight y<-c => z<=y $ +_L.2 $ inP (b, b<z, c, negative_L.2 y<-c, b+c>0)
    }
  }
  | join => join
  | join-left r => \case +_L.1 r \with {
    | inP (b,b<x,c,r,b+c>0) => LU-disjoint b<x $ U-closed (join_U.1 $ negative_L.1 r).1 linarith
  }
  | join-right r => \case +_L.1 r \with {
    | inP (b,b<y,c,r,b+c>0) => LU-disjoint b<y (U-closed (join_U.1 $ negative_L.1 r).2 linarith)
  }
  | join-univ x<=z y<=z r => \case +_L.1 r \with {
    | inP (b, e, c, z<-c, b+c>0) => \case join_L.1 e \with {
      | byLeft b<x => x<=z $ +_L.2 $ inP (b, b<x, c, z<-c, b+c>0)
      | byRight b<y => y<=z $ +_L.2 $ inP (b, b<y, c, z<-c, b+c>0)
    }
  }
  \where {
    \open OrderedSemiring

    \sfunc \infixl 6 + (x y : Real) : Real \cowith
      | LowerReal => x LowerRealAbMonoid.+ y
      | UpperReal => x UpperRealAbMonoid.+ y
      | LU-disjoint r r' => \case LowerRealAbMonoid.+_L.1 r, UpperRealAbMonoid.+_U.1 r' \with {
        | inP (a,a<x,b,b<y,q<a+b), inP (c,x<c,d,y<d,c+d<q) => linarith (x.LU-less a<x x<c, y.LU-less b<y y<d)
      }
      | LU-focus eps eps>0 => \case x.LU-focus (eps * ratio 1 4) linarith, y.LU-focus (eps * ratio 1 4) linarith \with {
        | inP (a,a<x,x<a+e/4), inP (b,b<y,y<b+e/4) => inP (a RatField.+ b - eps * ratio 1 4, LowerRealAbMonoid.+_L.2 $ inP (a, a<x, b, b<y, linarith), UpperRealAbMonoid.+_U.2 $ inP (_, x<a+e/4, _, y<b+e/4, linarith))
      }

    \lemma +_L {x y : Real} {a : Rat} : Real.L {x + y} a <-> ∃ (b : x.L) (c : y.L) (a < b RatField.+ c)
      => rewrite (\peval x + y, \peval x LowerRealAbMonoid.+ y) <->refl
      \where
        \lemma lower {x y : Real} : x + y = {LowerReal} x LowerRealAbMonoid.+ y
          => exts \lam a => <->_=.1 +_L *> inv (<->_=.1 LowerRealAbMonoid.+_L)

    \lemma +_U {x y : Real} {a : Rat} : Real.U {x + y} a <-> ∃ (b : x.U) (c : y.U) (b RatField.+ c < a)
      => rewrite (\peval x + y, \peval x UpperRealAbMonoid.+ y) <->refl
      \where
        \lemma upper {x y : Real} : x + y = {UpperReal} x UpperRealAbMonoid.+ y
          => exts \lam a => <->_=.1 +_U *> inv (<->_=.1 UpperRealAbMonoid.+_U)

    \lemma +-rat {x y : Rat} : x + y = {Real} x RatField.+ y
      => (\peval x + y) *> Real.real-lu-ext LowerRealAbMonoid.+-rat UpperRealAbMonoid.+-rat

    \sfunc negative (x : Real) : Real \cowith
      | L a => x.U (RatField.negative a)
      | L-inh => \case x.U-inh \with {
        | inP (a,x<a) => inP (RatField.negative a, simplify x<a)
      }
      | L-closed x<-q q'<q => x.U-closed x<-q (RatField.negative_< q'<q)
      | L-rounded x<-q => \case x.U-rounded x<-q \with {
        | inP (r,x<r,r<-q) => inP (RatField.negative r, simplify x<r, RatField.negative_<-right r<-q)
      }
      | U a => x.L (RatField.negative a)
      | U-inh => \case x.L-inh \with {
        | inP (a,a<x) => inP (RatField.negative a, simplify a<x)
      }
      | U-closed -q<x q<q' => x.L-closed -q<x (RatField.negative_< q<q')
      | U-rounded -q<x => \case x.L-rounded -q<x \with {
        | inP (r,r<x,-q<r) => inP (RatField.negative r, simplify r<x, RatField.negative_<-left -q<r)
      }
      | LU-disjoint p q => x.LU-disjoint q p
      | LU-located q<r => \case x.LU-located (RatField.negative_< q<r) \with {
        | byLeft -r<x => byRight -r<x
        | byRight x<-q => byLeft x<-q
      }

    \lemma negative_L {x : Real} {a : Rat} : Real.L {negative x} a <-> x.U (RatField.negative a)
      => rewrite (\peval negative x) <->refl

    \lemma negative_U {x : Real} {a : Rat} : Real.U {negative x} a <-> x.L (RatField.negative a)
      => rewrite (\peval negative x) <->refl

    \lemma negative-rat {x : Rat} : negative x = {Real} RatField.negative x
      => (\peval negative x) *> exts (\lam a => ext (\lam p => linarith, \lam p => linarith), \lam a => ext (\lam p => linarith, \lam p => linarith))

    \sfunc meet (x y : Real) : Real \cowith
      | LowerReal => LowerRealLattice.meet x y
      | UpperReal => UpperRealLattice.meet x y
      | LU-disjoint s r => \case UpperRealLattice.meet_U.1 r \with {
        | byLeft x<q => <-irreflexive (x.LU-less (LowerRealLattice.meet_L.1 s).1 x<q)
        | byRight y<q => <-irreflexive (y.LU-less (LowerRealLattice.meet_L.1 s).2 y<q)
      }
      | LU-located q<r => \case x.LU-located q<r, y.LU-located q<r \with {
        | byLeft q<x, byLeft q<y => byLeft $ LowerRealLattice.meet_L.2 (q<x,q<y)
        | _, byRight y<r => byRight $ UpperRealLattice.meet_U.2 (byRight y<r)
        | byRight x<r, _ => byRight $ UpperRealLattice.meet_U.2 (byLeft x<r)
      }

    \lemma meet_L {x y : Real} {a : Rat} : Real.L {meet x y} a <-> (\Sigma (x.L a) (y.L a))
      => rewrite (\peval meet x y, \peval LowerRealLattice.meet x y) <->refl

    \lemma meet_U {x y : Real} {a : Rat} : Real.U {meet x y} a <-> x.U a || y.U a
      => rewrite (\peval meet x y, \peval UpperRealLattice.meet x y) <->refl

    \sfunc join (x y : Real) : Real \cowith
      | LowerReal => LowerRealLattice.join x y
      | UpperReal => UpperRealLattice.join x y
      | LU-disjoint e s => \case LowerRealLattice.join_L.1 e \with {
        | byLeft q<x => <-irreflexive $ x.LU-less q<x (UpperRealLattice.join_U.1 s).1
        | byRight q<y => <-irreflexive $ y.LU-less q<y (UpperRealLattice.join_U.1 s).2
      }
      | LU-located q<r => \case x.LU-located q<r, y.LU-located q<r \with {
        | byLeft q<x, _ => byLeft $ LowerRealLattice.join_L.2 (byLeft q<x)
        | _, byLeft q<y => byLeft $ LowerRealLattice.join_L.2 (byRight q<y)
        | byRight x<r, byRight y<r => byRight $ UpperRealLattice.join_U.2 (x<r,y<r)
      }

    \lemma join_L {x y : Real} {a : Rat} : Real.L {join x y} a <-> x.L a || y.L a
      => rewrite (\peval join x y, \peval LowerRealLattice.join x y) <->refl

    \lemma join_U {x y : Real} {a : Rat} : Real.U {join x y} a <-> (\Sigma (x.U a) (y.U a))
      => rewrite (\peval join x y, \peval UpperRealLattice.join x y) <->refl

    \func half (x : Real) : Real \cowith
      | L a => x.L (a * 2)
      | L-inh => \case x.L-inh \with {
        | inP (a,a<x) => inP (a * ratio 1 2, transport x.L linarith a<x)
      }
      | L-closed c p => x.L-closed c linarith
      | L-rounded c => \case x.L-rounded c \with {
        | inP (a,a<x,q+q<a) => inP (a * ratio 1 2, transport x.L linarith a<x, linarith)
      }
      | U a => x.U (a * 2)
      | U-inh => \case x.U-inh \with {
        | inP (a,x<a) => inP (a * ratio 1 2, transport x.U linarith x<a)
      }
      | U-closed c p => x.U-closed c linarith
      | U-rounded c => \case x.U-rounded c \with {
        | inP (a,x<a,a<q+q) => inP (a * ratio 1 2, transport x.U linarith x<a, linarith)
      }
      | LU-disjoint => x.LU-disjoint
      | LU-located p => x.LU-located linarith

    \lemma half+half {x : Real} : half x + half x = x
      => Real.real-lu-ext (exts \lam a => <->_=.1 +_L *> ext (\lam (inP (b,b+b<x,c,c+c<x,a<b+c)) => \case dec<_<= a (b * 2), dec<_<= a (c * 2) \with {
        | inl a<b+b, _ => x.L-closed b+b<x a<b+b
        | _, inl a<c+c => x.L-closed c+c<x a<c+c
        | inr p, inr q => absurd linarith
      }, \lam a<x => \case x.L-rounded a<x \with {
        | inP (b,b<x,a<b) => inP (b * ratio 1 2, transport x.L linarith b<x, b * ratio 1 2, transport x.L linarith b<x, linarith)
      })) (exts \lam a => <->_=.1 +_U *> ext (\lam (inP (b,x<b+b,c,x<c+c,b+c<a)) => \case dec<_<= (b * 2) a, dec<_<= (c * 2) a \with {
        | inl b+b<a, _ => x.U-closed x<b+b b+b<a
        | _, inl c+c<a => x.U-closed x<c+c c+c<a
        | inr p, inr q => absurd linarith
      }, \lam x<a => \case x.U-rounded x<a \with {
        | inP (b,x<b,b<a) => inP (b * ratio 1 2, transport x.U linarith x<b, b * ratio 1 2, transport x.U linarith x<b, linarith)
      }))

    \lemma half>0 {x : Real} (x>0 : 0 RealAbGroup.< x) : 0 RealAbGroup.< half x
      => real_<_L.2 $ unfolds $ real_<_L.1 x>0

    \lemma half<id {x : Real} (x>0 : 0 RealAbGroup.< x) : half x RealAbGroup.< x
      => transport2 (RealAbGroup.<) zro-left half+half $ <_+-left (half x) (half>0 x>0)

    \lemma zro<ide : 0 RealAbGroup.< 1
      => real_<-rat-char.2 $ inP $ later (ratio 1 2, idp, idp)

    {-
    \lemma *'-char {x y : Real} {a : Rat} {b : Rat} (b<x : x.L b) {c : Rat} (c<y : y.L c) (b>=0 : 0 <= b) (c>=0 : 0 <= c) (a<=bc : a <= b * c)
      : ∃ (b : x.L) (c : y.L) (0 < b) (0 < c) (a < b * c)
      => \case x.L-rounded b<x, y.L-rounded c<y \with {
        | inP (b',b'<x,b<b'), inP (c',c'<y,c<c') => inP (b', b'<x, c', c'<y, b>=0 <∘r b<b', c>=0 <∘r c<c', a<=bc <∘r RatField.<=_*_positive-left (<_<= b<b') c>=0 <∘r <_*_positive-right (b>=0 <∘r b<b') c<c')
      }

    \func \infixl 7 *' {x y : Real} (x>0 : x.L 0) (y>0 : y.L 0) : Real \cowith
      | L a => ∃ (b : x.L) (c : y.L) (0 < b) (0 < c) (a < b * c)
      | L-inh => inP (0, *'-char x>0 y>0 <=-refl <=-refl <=-refl)
      | L-closed (inP (a,a<x,b,b<y,a>0,b>0,q<ab)) q'<q => inP (a, a<x, b, b<y, a>0, b>0, q'<q <∘ q<ab)
      | L-rounded (inP (a,a<x,b,b<y,a>0,b>0,q<ab)) => \case x.L-rounded a<x, y.L-rounded b<y \with {
        | inP (a',a'<x,a<a'), inP (b',b'<y,b<b') => inP (a' * b', *'-char a'<x b'<y (<_<= a>0 <=∘ <_<= a<a') (<_<= b>0 <=∘ <_<= b<b') <=-refl, q<ab <∘ RatField.<_*_positive-left a<a' b>0 <∘ <_*_positive-right (a>0 <∘ a<a') b<b')
      }
      | U a => ∃ (b : x.U) (c : y.U) (b * c < a)
      | U-inh => \case x.U-inh, y.U-inh \with {
        | inP (a,x<a), inP (b,y<b) => inP (a * b RatField.+ 1, inP (a, x<a, b, y<b, linarith))
      }
      | U-closed (inP (a,a<x,b,b<y,ab<q)) q<q' => inP (a, a<x, b, b<y, ab<q <∘ q<q')
      | U-rounded {q} (inP (a,a<x,b,b<y,ab<q)) => inP (RatField.mid (a * b) q, inP (a, a<x, b, b<y, RatField.mid>left ab<q), RatField.mid<right ab<q)
      | LU-disjoint (inP (a,a<x,b,b<y,a>0,b>0,q<ab)) (inP (c,x<c,d,y<d,cd<q)) => <-irreflexive $ q<ab <∘ RatField.<_*_positive-left (x.LU-less a<x x<c) b>0 <∘ <_*_positive-right (x.LU-less x>0 x<c) (y.LU-less b<y y<d) <∘ cd<q
      | LU-focus eps eps>0 => \case x.LU-focus 1 idp, y.LU-focus 1 idp \with {
        | inP (a,a<x,x<a+1), inP (b,b<y,y<b+1) =>
          \let | d1 => (eps * ratio 1 3) * finv (b RatField.+ 1) ∧ 1
               | d2 => finv (a RatField.+ 2) * (eps * ratio 1 3)
               | a+2>0 => x.LU-less x>0 $ x.U-closed x<a+1 $ <_+-right a idp
               | b+1>0 => y.LU-less y>0 y<b+1
               | d1>0 : 0 < d1 => <_meet-univ (<_*_positive_positive linarith $ RatField.finv>0 b+1>0) RatField.zro<ide
               | d2>0 : 0 < d2 => <_*_positive_positive (RatField.finv>0 a+2>0) linarith
          \in \case x.LU-focus d1 d1>0, y.LU-focus d2 d2>0 \with {
            | inP (a',a'<x,x<a'+d1), inP (b',b'<y,y<b'+d2) => inP ((a' ∨ 0) * (b' ∨ 0), *'-char (real_join_L a'<x x>0) (real_join_L b'<y y>0) join-right join-right <=-refl, inP ((a' ∨ 0) RatField.+ d1, x.U_<= x<a'+d1 $ RatField.<=_+ join-left <=-refl, (b' ∨ 0) RatField.+ d2, y.U_<= y<b'+d2 $ RatField.<=_+ join-left <=-refl,
                \have | lem1 : (a' ∨ 0) * d2 < eps * ratio 1 3 => transport2 (<) *-assoc ide-left $ <_*_positive-left (transport (_ <) (finv-right {_} {a RatField.+ 2} $ /=-sym $ RatField.<_/= a+2>0) $ <_*_positive-left (x.LU-less (real_join_L a'<x x>0) $ x.U-closed x<a+1 $ <_+-right a idp) $ RatField.finv>0 a+2>0) linarith
                      | lem2 : d1 * (b' ∨ 0) < eps * ratio 1 3 => RatField.<=_*_positive-left meet-left join-right <∘r transport2 (<) (inv *-assoc) ide-right (<_*_positive-right linarith $ transport (_ <) (RatField.finv-left {b RatField.+ 1} $ /=-sym $ RatField.<_/= b+1>0) $ <_*_positive-right (RatField.finv>0 b+1>0) $ y.LU-less (real_join_L b'<y y>0) y<b+1)
                      | lem3 : d1 * d2 < eps * ratio 1 3 => RatField.<=_*_positive-left meet-right (<_<= d2>0) <∘r transport2 (<) (inv ide-left) ide-left (<_*_positive-left (RatField.finv<1 $ linarith $ x.LU-less x>0 x<a+1) linarith)
                \in rewrite (RatField.ldistr,RatField.rdistr,RatField.+-assoc,RatField.rdistr) $ <_+-right _ linarith))
          }
      }
    -}
  }

{-
\instance RealField : OrderedField Real
  => {?}
  \where {
    \lemma diff-pos (x : Real) : ∃ (y z : Real) (y.L 0) (z.L 0) (x + y = z)
      => {?}

    \lemma diff-pos' (x : Real) : ∃ (y z : Real) (y.L 0) (z.L 0) (x = y - z)
      => \case x.LU-located { -1} {1} idp \with {
        | byLeft x>-1 => inP (x + 1, 1, unfold {?}, idp, inv zro-right *> pmap (x +) (inv negative-right) *> inv (RealAbGroup.+-assoc {_} {_} {RealAbGroup.negative 1}))
        | byRight x<1 => inP (1, Real.fromRat 1 - x, {?}, {?}, {?})
      }

    \open RealAbGroup(*',*'-char)

    \lemma \infixl 6 +' {x y : Real} (x>0 : x.L 0) (y>0 : y.L 0) : Real.L {x + y} 0
      => \case x.L-rounded x>0, y.L-rounded y>0 \with {
        | inP (a,a<x,a>0), inP (b,b<y,b>0) => inP (a, a<x, b, b<y, RatField.<_+ a>0 b>0)
      }

    \lemma rdistr' {x y z : Real} (x>0 : x.L 0) (y>0 : y.L 0) (z>0 : z.L 0) : (x>0 +' y>0) *' {x + y} z>0 = x>0 *' z>0 + y>0 *' z>0
      => exts (\lam a => ext (\lam (inP (b, inP (d,d<x,e,e<y,b<d+e), c, c<z, b>0, c>0, a<bc)) => inP (d RatField.* c, *'-char (real_join_L d<x x>0) c<z join-right (<_<= c>0) $ RatField.<=_*_positive-left join-left $ <_<= c>0, e RatField.* c, {?}, a<bc <∘ <_*_positive-left b<d+e c>0 <∘l Preorder.=_<= rdistr), {?}), {?})

    \lemma \infixl 7 *_ (x : Real) {y : Real} (y>0 : y.L 0)
      => TruncP.rec-set (diff-pos x) (\lam (x1,x2,x1>0,x2>0,p1) => x1>0 *' y>0 - x2>0 *' y>0) \lam s t => {?}

    \sfunc \infixl 7 * (x y : Real) : Real
      => (TruncP.rec-set (diff-pos x) (\lam (x1,x2,x1>0,x2>0,p1) => (TruncP.rec-set (diff-pos y) (\lam (y1,y2,y1>0,y2>0,p2) => x1>0 *' y1>0 + x2>0 *' y2>0 - (x1>0 *' y2>0 + x2>0 *' y1>0)) \lam s t => {?}).1) {?}).1
  }
-}

\open RealAbGroup(negative_L,+_L)

\lemma real_<-rat-char {x y : Real} : x < y <-> ∃ (a : Rat) (x.U a) (y.L a)
  => (\case +_L.1 __ \with {
        | inP (b,b<y,c,x<-c,b+c>0) => inP (b, x.U-closed (negative_L.1 x<-c) linarith, b<y)
      },
      \lam (inP (a,x<a,a<y)) => \case y.L-rounded a<y \with {
        | inP (b,b<y,a<b) => +_L.2 $ inP (b, b<y, negative a, negative_L.2 $ simplify x<a, linarith)
      })

\lemma real_<-char {x y : Real} : x < y <-> ∃ (a : Real) (x < a) (a < y)
  => (\lam x<y => \case real_<-rat-char.1 x<y \with {
        | (inP (a,x<a,a<y)) => inP (a, real_<_U.2 x<a, real_<_L.2 a<y)
      }, \lam (inP (a,x<a,a<y)) => x<a <∘ a<y)

\lemma real_<_L {a : Rat} {x : Real} : (a : Real) < x <-> x.L a
  => <->trans real_<-rat-char (\lam (inP (b,a<b,b<x)) => x.L-closed b<x a<b, \lam a<x => \case x.L-rounded a<x \with {
    | inP (b,b<x,a<b) => inP (b, a<b, b<x)
  })

\lemma real_<_U {a : Rat} {x : Real} : x < a <-> x.U a
  => <->trans real_<-rat-char (\lam (inP (b,x<b,b<a)) => x.U-closed x<b b<a, x.U-rounded)

\lemma rat_real_< {a b : Rat} : a < b <-> Real.fromRat a < Real.fromRat b
  => <->sym real_<_L

\lemma rat_real_<= {a b : Rat} : a <= b <-> Real.fromRat a <= Real.fromRat b
  => (\lam p q => p $ rat_real_<.2 q, \lam p q => p $ rat_real_<.1 q)

\lemma rat_real_meet {a b : Rat} : Real.fromRat (a ∧ b) = Real.fromRat a ∧ Real.fromRat b
  => <=-antisymmetric (meet-univ (rat_real_<=.1 meet-left) (rat_real_<=.1 meet-right)) \case TotalOrder.meet-isMin a b \with {
    | byLeft p => rewrite p meet-left
    | byRight p => rewrite p meet-right
  }

\lemma rat_real_join {a b : Rat} : Real.fromRat (a ∨ b) = Real.fromRat a ∨ Real.fromRat b
  => <=-antisymmetric (\case TotalOrder.join-isMax a b \with {
    | byLeft p => rewrite p RealAbGroup.join-left
    | byRight p => rewrite p RealAbGroup.join-right
  }) (join-univ (rat_real_<=.1 join-left) (rat_real_<=.1 join-right))

\lemma rat_real_abs {a : Rat} : Real.fromRat (RatField.abs a) = RealAbGroup.abs (Real.fromRat a)
  => rat_real_join *> pmap (_ RealAbGroup.∨) (inv RealAbGroup.negative-rat)

\instance RealDenseOrder : UnboundedDenseLinearOrder
  | LinearOrder => RealAbGroup
  | isDense x<z => \case real_<-rat-char.1 x<z \with {
    | inP (a,x<a,a<z) => inP (a, real_<_U.2 x<a, real_<_L.2 a<z)
  }
  | withoutUpperBound x => \case U-inh {x} \with {
    | inP (a,x<a) => inP (a, real_<_U.2 x<a)
  }
  | withoutLowerBound x => \case L-inh {x} \with {
    | inP (a,a<x) => inP (a, real_<_L.2 a<x)
  }

\lemma <=_L-char {x y : Real} : x <= y <-> (\Pi {a : Rat} -> x.L a -> y.L a)
  => (\lam h a<x => \case L-rounded a<x \with {
    | inP (b,b<x,a<b) => \case y.LU-located a<b \with {
      | byLeft a<y => a<y
      | byRight y<b => absurd $ h $ real_<-rat-char.2 $ inP (b,y<b,b<x)
    }
  }, \lam f p => \case real_<-rat-char.1 p \with {
    | inP (a,y<a,a<x) => y.LU-disjoint (f a<x) y<a
  })

\lemma <=_U-char {x y : Real} : x <= y <-> (\Pi {a : Rat} -> y.U a -> x.U a)
  => (\lam h y<a => \case U-rounded y<a \with {
    | inP (b,y<b,b<a) => \case x.LU-located b<a \with {
      | byLeft b<x => absurd $ h $ real_<-rat-char.2 $ inP (b,y<b,b<x)
      | byRight x<a => x<a
    }
  }, \lam f p => \case real_<-rat-char.1 p \with {
    | inP (a,y<a,a<x) => x.LU-disjoint a<x (f y<a)
  })

\lemma real-located {x a b : Real} (p : a < b) : a < x || x < b
  => \case real_<-rat-char.1 p \with {
    | inP (a',a<a',a'<b) => \case L-rounded a'<b \with {
      | inP (b',b'<b,a'<b') => \case x.LU-located a'<b' \with {
        | byLeft a'<x => byLeft $ real_<-rat-char.2 $ inP (a', a<a', a'<x)
        | byRight x<b' => byRight $ real_<-rat-char.2 $ inP (b', x<b', b'<b)
      }
    }
  }

\lemma real-focus (x : Real) {eps : Real} (eps>0 : 0 < eps) : ∃ (a : Real) (a < x) (x < a + eps)
  => \case real_<-rat-char.1 eps>0 \with {
    | inP (eps',eps'>0,eps'<eps) => \case x.LU-focus eps' eps'>0 \with {
      | inP (a,a<x,x<a+eps') => inP (a, real_<_L.2 a<x, real_<_U.2 x<a+eps' <∘ rewriteI RealAbGroup.+-rat (RealAbGroup.<_+-right a $ real_<_L.2 eps'<eps))
    }
  }

\lemma real_join_L {a b : Rat} {x : Real} (a<x : x.L a) (b<x : x.L b) : x.L (a ∨ b)
  => \case TotalOrder.join-isMax a b \with {
    | byLeft p => rewrite p a<x
    | byRight p => rewrite p b<x
  }

\lemma real_meet_U {a b : Rat} {x : Real} (x<a : x.U a) (x<b : x.U b) : x.U (a ∧ b)
  => \case TotalOrder.meet-isMin a b \with {
    | byLeft p => rewrite p x<a
    | byRight p => rewrite p x<b
  }