\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.MonoidHom
\import Algebra.Ordered
\import Algebra.StrictlyOrdered
\import Algebra.Pointed
\import Arith.Int
\import Arith.Nat
\import Arith.Rat
\import Data.Or
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Biordered
\import Order.Lattice
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Set

\record ExUpperReal (U : Rat -> \Prop) {
  | 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 RatField.<= r) : U r
    => \case LinearOrder.<=-dec p \with {
      | inl q<r => U-closed Uq q<r
      | inr q=r => transport U q=r Uq
    }

  \func IsBounded : \Prop
    => ∃ U
} \where {
  \use \coerce fromRat (x : Rat) : ExUpperReal \cowith
    | U => x <
    | U-closed => <∘
    | U-rounded => isDense

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

  \sfunc \infixl  + (x y : ExUpperReal) : ExUpperReal \cowith
    | U a => ∃ (b : x.U) (c : y.U) (b RatField.+ c RatField.< a)
    | 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 : ExUpperReal} {a : Rat} : UpperReal.U {x + y} a <-> ∃ (b : x.U) (c : y.U) (b RatField.+ c RatField.< a)
    => rewrite (\peval x + y) <->refl

  \lemma +_U_<= {x y : ExUpperReal} {a : Rat} : UpperReal.U {x + y} a <-> ∃ (b : x.U) (c : y.U) (b RatField.+ c RatField.<= a)
    => <->trans +_U $ later (\lam (inP (b,x<b,c,y<c,b+c<a)) => inP (b, x<b, c, y<c, RatField.<=-less b+c<a), \lam (inP (b,x<b,c,y<c,b+c<=a)) => \case U-rounded x<b \with {
      | inP (b',x<b',b'<b) => inP (b', x<b', c, y<c, <_+-left c b'<b RatField.<∘l b+c<=a)
    })

  \lemma +-rat {x y : Rat} : fromRat x + fromRat y = fromRat (x RatField.+ y)
    => (\peval _ + _) *> 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) RatField.* ratio  , linarith, y - (x RatField.+ y - a) RatField.* ratio  , linarith, linarith))

  \type \infix  <= (x y : ExUpperReal) => ∀ {b : y.U} (x.U b)

  \lemma <=_+-char {x y z : ExUpperReal} {a b : Rat} (x<=y+z : x <= y + z) (y<a : y.U a) (z<b : z.U b) : x.U (a RatField.+ b)
    => x<=y+z $ +_U_<=. $ inP (a,y<a,b,z<b,<=-refl)

  \lemma <=-rat {a b : Rat} : a RatField.<= b <-> a <= b
    => (\lam a<=b {c} b<c => a<=b RatField.<∘r b<c, \lam a<=b b<a => <-irreflexive (a<=b b<a))

  \protected \lemma <_<= {x : ExUpperReal} {q : Rat} (x<q : x.U q) : x <= q
    => U-closed x<q __

  \sfunc meet (x y : ExUpperReal) : ExUpperReal \cowith
    | U a => x.U a || y.U 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 : ExUpperReal} {a : Rat} : UpperReal.U {meet x y} a <-> x.U a || y.U a
    => rewrite (\peval meet x y) <->refl

  \sfunc join (x y : ExUpperReal) : ExUpperReal \cowith
    | U a => \Sigma (x.U a) (y.U a)
    | 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), RatField.<_join-univ q<r q<r')
    }

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

  \lemma join-bounded {x y : ExUpperReal} (xb : x.IsBounded) (yb : y.IsBounded) : (join x y).IsBounded \elim xb, yb
    | inP (a,x<a), inP (b,y<b) => inP (a ∨ b, join_U. (x.U_<= x<a join-left, y.U_<= y<b join-right))

  \sfunc \infixl  * (x y : ExUpperReal) : ExUpperReal \cowith
    | U a => ∃ (b : x.U) ( RatField.< b) (c : y.U) ( RatField.< c) (b RatField.* c RatField.< a)
    | U-closed (inP (b,x<b,b>0,c,y<c,c>0,bc<q)) q<q' => inP (b, x<b, b>0, c, y<c, c>0, bc<q <∘ q<q')
    | U-rounded (inP (b,x<b,b>0,c,y<c,c>0,bc<q)) => inP (_, inP (b, x<b, b>0, c, y<c, c>0, RatField.mid>left bc<q), RatField.mid<right bc<q)

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

  \lemma *_U_<= {x y : ExUpperReal} {a : Rat} : UpperReal.U {x * y} a <-> ∃ (b : x.U) ( RatField.< b) (c : y.U) ( RatField.< c) (b RatField.* c RatField.<= a)
    => (\lam xy<a => \case *_U. xy<a \with {
      | inP (b,x<b,b>0,c,y<c,c>0,bc<a) => inP (b, x<b, b>0, c, y<c, c>0, <=-less bc<a)
    }, \lam (inP (b,x<b,b>0,c,y<c,c>0,bc<=a)) => \case U-rounded x<b \with {
      | inP (b',x<b',b'<b) => *_U. $ inP (b' ∨ RatField.mid  b, ExUpperReal.U_<= x<b' join-left, RatField.mid>left b>0 <∘l join-right, c, y<c, c>0, <_*_positive-left (<_join-univ b'<b $ RatField.mid<right b>0) c>0 <∘l bc<=a)
    })

  \lemma *_U_< {x y : ExUpperReal} {a : Rat} : UpperReal.U {x * y} a <-> ∃ (b : Rat) (x <= b) ( RatField.<= b) (c : Rat) (y <= c) ( RatField.<= c) (b RatField.* c < a)
    => <->trans *_U $ later (\lam (inP (b,x<b,b>0,c,y<c,c>0,bc<a)) => inP (b, <_<= x<b, <=-less b>0, c, <_<= y<c, <=-less c>0, bc<a), \lam (inP (b,x<=b,b>=0,c,y<=c,c>=0,bc<a)) => \case LinearOrder.dec<_<=  c \with {
      | inl c>0 =>
        \let | b' => RatField.mid b (RatField.finv c RatField.* a)
             | bp => transport (_ <) *-comm (RatField.<_rotate-right c>0 bc<a)
             | b'>0 => b>=0 <∘r RatField.mid>left bp
             | c' => RatField.mid c (a RatField.* RatField.finv b')
             | cp => RatField.<_rotate-right b'>0 $ transport (`< _) *-comm $ RatField.<_rotate-right-conv c>0 $ transport (_ <) *-comm (RatField.mid<right bp)
        \in inP (b', x<=b $ RatField.mid>left bp, b'>0, c', y<=c $ RatField.mid>left cp, c>0 <∘ RatField.mid>left cp, transport2 (<) *-comm (*-assoc *> pmap (a RatField.*) (RatField.finv-left $ RatField.>_/= b'>0) *> ide-right) $ RatField.<_*_positive-left (RatField.mid<right cp) b'>0)
      | inr c<=0 =>
        \let | c' => RatField.half (a RatField.* RatField.finv (b RatField.+ ))
             | b'>0 :  < b RatField.+  => linarith
             | c'2>0 => RatField.<_*_positive_positive (transport (`< a) (pmap (b RatField.*) (<=-antisymmetric c<=0 c>=0) *> RatField.zro_*-right) bc<a) (RatField.finv>0 b'>0)
        \in inP (b RatField.+ , x<=b linarith, b'>0, c', y<=c $ c<=0 <∘r RatField.half>0 c'2>0, RatField.half>0 c'2>0, transport (`< _) *-comm $ RatField.<_rotate-right-conv b'>0 $ RatField.half<id c'2>0)
    })

  \lemma *-rat {x y : Rat} (x>=0 :  RatField.<= x) (y>=0 :  RatField.<= y) : fromRat x * fromRat y = fromRat (x RatField.* y)
    => ExUpperRealAbMonoid.<=-antisymmetric (\lam {d} xy<d => *_U_<. $ inP (x, <=-rat. <=-refl, x>=0, y, <=-rat. <=-refl, y>=0, xy<d)) (\lam {d} xy<d => \case *_U. xy<d \with {
      | inP (a,x<a,a>0,b,y<b,b>0,ab<d) => RatField.<=_*_positive-left (<=-less x<a) y>=0 <∘r <=-less (<_*_positive-right a>0 y<b) <∘r ab<d
    })
}

\instance ExUpperRealPointed : Pointed ExUpperReal
  | ide => ExUpperReal.fromRat 

\lemma real_meet_U {a b : Rat} {x : ExUpperReal} (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
  }

\instance ExUpperRealAbMonoid : BiorderedLatticeAbMonoid ExUpperReal
  | zro => ExUpperReal.fromRat 
  | + => +
  | 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) RatField.* ratio  , linarith, b, b<x, linarith)
  })
  | +-assoc => exts \lam a => ext (\lam r => \case +_U. r \with {
    | inP (b, r', c, c<z,a<b+c) => \case +_U. r' \with {
      | inP (d,d<x,e,e<y,b<d+e) => +_U. $ inP (d, d<x, (a - d RatField.+ c RatField.+ e) RatField.* ratio  , +_U. $ inP (e, e<y, c, c<z, linarith), linarith)
    }
  }, \lam r => \case +_U. r \with {
    | inP (b, b<x, c, r', a<b+c) => \case +_U. r' \with {
      | inP (d,d<y,e,e<z,c<d+e) => +_U. $ inP ((a - e RatField.+ b RatField.+ d) RatField.* ratio  , +_U. $ inP (b, b<x, d, d<y, linarith), e, e<z, linarith)
    }
  })
  | +-comm => exts \lam a => ext (\lam r => \case +_U. r \with {
    | inP (b,b<x,c,c<y,a<b+c) => +_U. $ inP $ later (c, c<y, b, b<x, rewrite RatField.+-comm a<b+c)
  }, \lam r => \case +_U. r \with {
    | inP (c,c<y,b,b<x,a<c+b) => +_U. $ inP $ later (b, b<x, c, c<y, rewrite RatField.+-comm a<c+b)
  })
  | <= => <=
  | <=-refl x<a => x<a
  | <=-transitive p q x<a => p (q x<a)
  | <=-antisymmetric p q => exts \lam a => ext (q,p)
  | <=_+ p q {x} r => \case +_U. r \with {
    | inP (b',b<b',d',d<d',b'+d'<x) => +_U. $ inP (b', p b<b', d', q d<d', b'+d'<x)
  }
  | < => <
  | <-irreflexive (inP (q,x<q,q<=x)) => <-irreflexive (q<=x x<q)
  | <-transitive (inP (a,x<a,a<=y)) (inP (b,y<b,b<=z)) => inP (a, x<a, \lam {c} z<c => a<=y y<b <∘ b<=z z<c)
  | <-transitive-right e (inP (b,a2<b,b<=a3)) => inP (b, e a2<b, b<=a3)
  | <-transitive-left (inP (b,a1<b,b<=a2)) e => inP (b, a1<b, \lam {c} a3<c => b<=a2 (e a3<c))
  | <=-less (inP (q,a1<q,q<=a2)) a2<b => U-closed a1<q (q<=a2 a2<b)
  | meet => meet
  | meet-left x<a => meet_U. (byLeft x<a)
  | meet-right y<a => meet_U. (byRight y<a)
  | meet-univ x<=z y<=z r => \case meet_U. r \with {
    | byLeft a<x => x<=z a<x
    | byRight a<y => y<=z a<y
  }
  | join => join
  | join-left s => (join_U. s).
  | join-right s => (join_U. s).
  | join-univ z<=x z<=y a<z => join_U. (z<=x a<z, z<=y a<z)
  | <_meet-univ (inP (a,x<a,a<=y)) (inP (b,x<b,b<=z)) => inP (a ∧ b, real_meet_U x<a x<b, \lam {w} r => \case meet_U. r \with {
    | byLeft y<w => meet-left <∘r a<=y y<w
    | byRight z<w => meet-right <∘r b<=z z<w
  })
  | <_join-univ (inP (a,x<a,a<=z)) (inP (b,y<b,b<=z)) => inP (a ∨ b, join_U. (U_<= x<a join-left, U_<= y<b join-right), \lam {w} z<w => <_join-univ (a<=z z<w) (b<=z z<w))
  | meet_+-left => exts \lam x => ext (\lam r => \case +_U. r \with {
    | inP (a',a<a',d,bc<d,a'+d<x) => \case meet_U. bc<d \with {
      | byLeft b<d => meet_U. $ byLeft $ +_U. $ inP (a', a<a', d, b<d, a'+d<x)
      | byRight c<d => meet_U. $ byRight $ +_U. $ inP (a', a<a', d, c<d, a'+d<x)
    }
  }, \lam r => \case meet_U. r \with {
    | byLeft a+b<x => \case +_U. a+b<x \with {
      | inP (a',a<a',b',b<b',a'+b'<x) => +_U. $ inP (a', a<a', b', meet_U. $ byLeft b<b', a'+b'<x)
    }
    | byRight a+c<x => \case +_U. a+c<x \with {
      | inP (a',a<a',c',c<c',a'+c'<x) => +_U. $ inP (a', a<a', c', meet_U. $ byRight c<c', a'+c'<x)
    }
  })
  | join_+-left => exts \lam x => ext (\lam r => \case +_U. r \with {
    | inP (a',a<a',d,bc<d,a'+d<x) => \case join_U. bc<d \with {
      | (b<d,c<d) => join_U. (+_U. $ inP (a', a<a', d, b<d, a'+d<x), +_U. $ inP (a', a<a', d, c<d, a'+d<x))
    }
  }, \lam r => \case join_U. r \with {
    | (a+b<x,a+c<x) => \case +_U. a+b<x, +_U. a+c<x \with {
      | inP (a1,a<a1,b',b<b',a1+b'<x), inP (a2,a<a2,c',c<c',a2+c'<x) => +_U. $ inP (a1 ∧ a2, real_meet_U a<a1 a<a2, b' ∨ c', join_U. (U_<= b<b' join-left, U_<= c<c' join-right), later $ rewrite RatField.join_+-left $ <_join-univ (<=_+ meet-left <=-refl <∘r a1+b'<x) (<=_+ meet-right <=-refl <∘r a2+c'<x))
    }
  })
  \where {
    \open ExUpperReal

    \type \infix  < (x y : ExUpperReal) => ∃ (q : x.U) (q ExUpperReal.<= y)

    \lemma <-rat {x : ExUpperReal} {y : Rat} : x < y <-> x.U y
      => (\lam (inP (q,x<q,q<=y)) => x.U_<= x<q $ <=-rat. q<=y, \lam x<y => inP (y, x<y, ExUpperRealAbMonoid.<=-refl))

    \lemma zro<ide : fromRat  < fromRat 
      => inP (, idp, ExUpperRealAbMonoid.<=-refl)

    \lemma <_+ {x y x' y' : ExUpperReal} (x<x' : x < x') (y<y' : y < y') : x + y < x' + y' \elim x<x', y<y'
      | inP (a,x<a,a<=x'), inP (b,y<b,b<=y') => inP (a RatField.+ b, +_U_<=. $ inP (a,x<a,b,y<b,<=-refl), transport (`<= _) +-rat $ ExUpperRealAbMonoid.<=_+ a<=x' b<=y')

    \lemma <_+-left {x y : ExUpperReal} (x<y : x < y) {z : Rat} : x + z < y + z \elim x<y
      | inP (a,x<a,a<=y) => inP (a RatField.+ z, \case U-rounded x<a \with {
        | inP (b,x<b,b<a) => +_U_<=. $ inP (b, x<b, z RatField.+ a - b, linarith, linarith)
      }, transport (`<= _) +-rat $ ExUpperRealAbMonoid.<=_+ a<=y ExUpperRealAbMonoid.<=-refl)

    \lemma <_+-right {x : Rat} {y z : ExUpperReal} (y<z : y < z) : x + y < x + z
      => transport2 (<) ExUpperRealAbMonoid.+-comm ExUpperRealAbMonoid.+-comm (<_+-left y<z)

    \lemma <=_+-cancel-left {x y z : ExUpperReal} (xb : x.IsBounded) {q : Rat} (q<=x : q <= x) (p : x + y <= x + z) : y <= z \elim xb
      | inP (B,x<B) => \lam {b} z<b => \case U-rounded z<b \with {
        | inP (b',z<b',b'<b) =>
          \have N => rat_natBound $ RatField.finv (b - b') RatField.* (B - q)
          \in \case steps (RatField.to>0 b'<b) x<B z<b' N. \with {
            | byLeft r => absurd $ <-irreflexive $ RatField.<-diff-left (RatField.<_rotate-left-conv (RatField.to>0 b'<b) N.) <∘ q<=x r
            | byRight r => transport y.U linarith r
          }
      }
      \where \private {
        \lemma step {eps : Rat} (eps>0 :  RatField.< eps) {a : Rat} (x<a : x.U a) {b : Rat} (z<b : z.U b) : x.U (a - eps) || y.U (b RatField.+ eps)
          => \case +_U. $ p $ +_U_<=. $ inP (a, x<a, b, z<b, <=-refl) \with {
            | inP (a',x<a',b',y<b',a'+b'<a+b) => \case LinearOrder.dec<_<= (a - eps) a' \with {
              | inl a-eps<a' => byRight $ U-closed y<b' linarith
              | inr a'<=a-eps => byLeft $ x.U_<= x<a' a'<=a-eps
            }
          }

        \lemma steps {eps : Rat} (eps>0 :  RatField.< eps) {a : Rat} (x<a : x.U a) {b : Rat} (z<b : z.U b) (n : Nat) : x.U (a - eps RatField.* n) || y.U (b RatField.+ eps) \elim n
          |  => byLeft $ transport x.U linarith x<a
          | suc n => \case step eps>0 x<a z<b \with {
            | byLeft x<a-eps => \case steps eps>0 x<a-eps z<b n \with {
              | byLeft r => byLeft $ transport x.U (+-assoc *> pmap (a RatField.+) (inv RatField.negative_+ *> pmap negative (pmap (_ RatField.+) (inv ide-right) *> inv RatField.ldistr))) r
              | byRight r => byRight r
            }
            | byRight r => byRight r
          }
      }

    \lemma <=_+-cancel-right {x y z : ExUpperReal} (zb : z.IsBounded) {q : Rat} (q<=z : q <= z) (p : x + z <= y + z) : x <= y
      => <=_+-cancel-left zb q<=z $ transport2 (<=) ExUpperRealAbMonoid.+-comm ExUpperRealAbMonoid.+-comm p

    \lemma *n_U {n : Nat} (n/=0 : n /= ) {x : ExUpperReal} {q : Rat} : (n ExUpperRealAbMonoid.*n x).U q <-> ∃ (r : x.U) (n RatField.* r RatField.<= q) \elim n
      |  => absurd (n/=0 idp)
      |  => rewrite zro-left (\lam x<q => inP (q, x<q, =_<= ide-left), \lam (inP (r,x<r,r<=q)) => x.U_<= x<r $ rewrite RatField.ide-left in r<=q)
      | suc (suc n) => (\lam c => \case +_U_<=. c \with {
        | inP (a,ap,b,x<b,a+b<=q) => \case (*n_U {suc n} suc/=0). ap \with {
          | inP (r,x<r,rp) => inP (b ∧ r, real_meet_U x<b x<r, =_<= (RatField.rdistr {suc n}) <=∘ <=_+ (RatField.<=_*_positive-right rat_<=-dec meet-right <=∘ rp) (=_<= ide-left <=∘ meet-left) <=∘ a+b<=q)
        }
      }, \lam (inP (r,x<r,rp)) => +_U_<=. $ inP (suc n RatField.* r, (*n_U {suc n} suc/=0 {x} {suc n RatField.* r}). $ inP (r,x<r,<=-refl), r, x<r, =_<= (inv $ RatField.rdistr *> pmap (_ RatField.+) ide-left) <=∘ rp))

    \lemma *n_finv {n : Nat} (n/=0 : n /= ) {x : ExUpperReal} {q : Rat} : (n ExUpperRealAbMonoid.*n x).U q <-> x.U (RatField.finv n RatField.* q)
      => <->trans (*n_U n/=0) (
        \lam (inP (r,x<r,nr<=q)) => x.U_<= x<r $ =_<= (inv (pmap (RatField.`* r) (RatField.finv-left $ natRat/=0 n/=0) *> ide-left) *> *-assoc) <=∘ RatField.<=_*_positive-right (RatField.finv>=0 fromNat_>=0) nr<=q,
        \lam x<q/n => inP (_, x<q/n, =_<= $ inv *-assoc *> pmap (RatField.`* q) (RatField.finv-right $ natRat/=0 n/=0) *> ide-left))
  }

\lemma rat-upperReal : AddMonoidHom RatField ExUpperRealAbMonoid ExUpperReal.fromRat \cowith
  | func-zro => idp
  | func-+ => inv ExUpperReal.+-rat

\instance ExUpperRealSemigroup : CSemigroup ExUpperReal
  | * => *
  | *-assoc => <=-antisymmetric (\lam {d} xyz<d => \case *_U. xyz<d \with {
    | inP (a,x<a,a>0,b',yz<b',_,ab'<d) => \case *_U. yz<b' \with {
      | inP (b,y<b,b>0,c,z<c,c>0,bc<b') => *_U. $ inP (a RatField.* b, *_U_<=. $ inP (a,x<a,a>0,b,y<b,b>0,<=-refl), RatField.<_*_positive_positive a>0 b>0, c, z<c, c>0, transportInv (RatField.`< _) *-assoc $ RatField.<_*_positive-right a>0 bc<b' <∘ ab'<d)
    }
  }) (\lam {d} xyz<d => \case *_U. xyz<d \with {
    | inP (a',xy<a',_,c,z<c,c>0,a'c<d) => \case *_U. xy<a' \with {
      | inP (a,x<a,a>0,b,y<b,b>0,ab<a') => *_U. $ inP (a, x<a, a>0, b RatField.* c, *_U_<=. $ inP (b,y<b,b>0,c,z<c,c>0,<=-refl), RatField.<_*_positive_positive b>0 c>0, transport (RatField.`< _) *-assoc $ RatField.<_*_positive-left ab<a' c>0 <∘ a'c<d)
    }
  })
  | *-comm => \have lem {x} {y} : x * y <= y * x => \lam {d} yx<d => \case *_U. yx<d \with {
    | inP (b,y<b,b>0,a,x<a,a>0,ba<d) => *_U. $ inP (a, x<a, a>0, b, y<b, b>0, transport (RatField.`< _) *-comm ba<d)
  } \in <=-antisymmetric lem lem
  \where {
    \open ExUpperReal

    \protected \lemma ide-left_<= {x : ExUpperReal} : x <= fromRat  * x
      => \lam {a} p => \case *_U. p \with {
        | inP (b,b>1,_,c,x<c,c>0,bc<a) => U-closed x<c $ transport (RatField.`< _) RatField.ide-left (<_*_positive-left b>1 c>0) <∘ bc<a
      }

    \protected \lemma ide-left {x : ExUpperReal} (x>=0 :  <= x) : fromRat  * x = x
      => <=-antisymmetric (\lam {a} x<a => \case U-rounded x<a \with {
        | inP (b,x<b,b<a) => *_U_<=. $ inP $ later (a RatField.* RatField.finv b, transport (RatField.`< _) (RatField.finv-right $ RatField.>_/= $ x>=0 x<b) $ <_*_positive-left b<a $ RatField.finv>0 (x>=0 x<b), RatField.<_*_positive_positive (x>=0 x<a) (RatField.finv>0 $ x>=0 x<b), b, x<b, x>=0 x<b, =_<= $ *-assoc *> pmap (a RatField.*) (RatField.finv-left $ RatField.>_/= $ x>=0 x<b) *> RatField.ide-right)
      }) ide-left_<=

    \protected \lemma ide-right {x : ExUpperReal} (x>=0 :  <= x) : x * fromRat  = x
      => ExUpperRealSemigroup.*-comm *> ide-left x>=0

    \lemma <=_* {x x' y y' : ExUpperReal} (x<=x' : x <= x') (y<=y' : y <= y') : x * y <= x' * y'
      => \lam {d} x'y'<d => \case *_U. x'y'<d \with {
        | inP (a,x'<a,a>0,b,y'<b,b>0,ab<d) => *_U. $ inP (a, x<=x' x'<a, a>0, b, y<=y' y'<b, b>0, ab<d)
      }

    \lemma *_join {x y : ExUpperReal} : x * y = join x  * join y 
      => <=-antisymmetric (<=_* join-left join-left) \lam {d} xy<d => \case *_U. xy<d \with {
        | inP (a,x<a,a>0,b,y<b,b>0,ab<d) => *_U. $ inP (a, join_U. (x<a,a>0), a>0, b, join_U. (y<b,b>0), b>0, ab<d)
      }

    \lemma <_* {x x' y y' : ExUpperReal} (x>=0 :  <= x) (y>=0 :  <= y) (x<x' : x < x') (y<y' : y < y') : x * y < x' * y' \elim x<x', y<y'
      | inP (a,x<a,a<=x'), inP (b,y<b,b<=y') => inP (a RatField.* b, *_U_<=. $ inP (a, x<a, x>=0 x<a, b, y<b, y>=0 y<b, <=-refl), transport (`<= _) (*-rat (<=-less $ x>=0 x<a) (<=-less $ y>=0 y<b)) $ <=_* a<=x' b<=y')

    \lemma <_*_U-left {x : ExUpperReal} {y z : Rat} (x<y : x.U y) (y>0 :  RatField.< y) (z>0 :  RatField.< z) : (x * z).U (y RatField.* z)
      => \case U-rounded x<y \with {
        | inP (y',x<y',y'<y) =>
          \let | y1 => y' ∨ 
               | x<y1 => U_<= x<y' join-left
               | y1<y => <_join-univ y'<y y>0
               | xz<=y1z => transport (_ <=) (*-rat join-right $ <=-less z>0) $ <=_* (ExUpperReal.<_<= x<y1) <=-refl
          \in xz<=y1z $ RatField.<_*_positive-left y1<y z>0
      }

    \lemma <_*_U-right {x : Rat} (x>0 :  RatField.< x) {y : ExUpperReal} {z : Rat} (z>0 :  RatField.< z) (y<z : y.U z) : (x * y).U (x RatField.* z)
      => rewrite (ExUpperRealSemigroup.*-comm, RatField.*-comm) (<_*_U-left y<z z>0 x>0)

    \lemma <_*-left {x y : ExUpperReal} (x<y : x < y) (y>0 :  < y) {z : Rat} (z>0 :  RatField.< z) : x * z < y * z
      => \case <_join-univ x<y y>0 \with {
        | inP (q,qp,q<=y) => \have q>0 => ExUpperRealAbMonoid.join-right qp
                             \in <-rat. (<_*_U-left (ExUpperRealAbMonoid.join-left qp) q>0 z>0) <∘l transport (`<= _) (*-rat (<=-less q>0) (<=-less z>0)) (<=_* q<=y <=-refl)
      }

    \lemma <_*-right {x : Rat} (x>0 :  RatField.< x) {y z : ExUpperReal} (y<z : y < z) (z>0 :  < z) : x * y < x * z
      => transport2 (<) ExUpperRealSemigroup.*-comm ExUpperRealSemigroup.*-comm (<_*-left y<z z>0 x>0)

    \lemma <_*-left' {x y : ExUpperReal} (x<y : x < y) (x>=0 :  <= x) {z : Rat} (z>0 :  RatField.< z) : x * z < y * z
      => <_*-left x<y (x>=0 <∘r x<y) z>0

    \lemma <_*-right' {x : Rat} (x>0 :  RatField.< x) {y z : ExUpperReal} (y<z : y < z) (y>=0 :  <= y) : x * y < x * z
      => <_*-right x>0 y<z (y>=0 <∘r y<z)

    \lemma *_>=0 {x y : ExUpperReal} :  <= x * y
      => \lam {d} xy<d => \case *_U. xy<d \with {
        | inP (a,x<a,a>0,b,y<b,b>0,ab<d) => RatField.<_*_positive_positive a>0 b>0 <∘ ab<d
      }

    \protected \lemma ldistr_<= {x y z : ExUpperReal} : x * (y + z) <= x * y + x * z
      => \lam {d} xy+xz<d => \case +_U. xy+xz<d \with {
        | inP (b',xy<b',c',xz<c',b'+c'<d) => \case *_U. xy<b', *_U. xz<c' \with {
          | inP (a1,x<a1,a1>0,b,y<b,b>0,a1b<b'), inP (a2,x<a2,a2>0,c,z<c,c>0,a2c<c') => *_U. $ inP (
              a1 ∧ a2, real_meet_U x<a1 x<a2, <_meet-univ a1>0 a2>0, b RatField.+ c, +_U_<=. $ inP (b,y<b,c,z<c,<=-refl), linarith,
              transportInv (RatField.`< _) RatField.ldistr (RatField.<_+ (RatField.<=_*_positive-left meet-left (<=-less b>0) <∘r a1b<b') (RatField.<=_*_positive-left meet-right (<=-less c>0) <∘r a2c<c')) <∘ b'+c'<d)
        }
      }

    \protected \lemma rdistr_<= {x y z : ExUpperReal} : (x + y) * z <= x * z + y * z
      => transport (`<= _) ExUpperRealSemigroup.*-comm $ ldistr_<= <=∘ =_<= (pmap2 (+) ExUpperRealSemigroup.*-comm ExUpperRealSemigroup.*-comm)

    \protected \lemma ldistr {x y z : ExUpperReal} (y>=0 :  <= y) (z>=0 :  <= z) : x * (y + z) = x * y + x * z
      => <=-antisymmetric ldistr_<= \lam {d} x[y+z]<d => \case *_U. x[y+z]<d \with {
        | inP (a,x<a,a>0,d',y+z<d',d'>0,ad'<d) => \case +_U. y+z<d' \with {
          | inP (b,y<b,c,z<c,b+c<d') => +_U. $ inP (a RatField.* b, *_U_<=. $ inP (a, x<a, a>0, b, y<b, y>=0 y<b, <=-refl), a RatField.* c, *_U_<=. $ inP (a, x<a, a>0, c, z<c, z>=0 z<c, <=-refl), transport (RatField.`< _) RatField.ldistr (RatField.<_*_positive-right a>0 b+c<d') <∘ ad'<d)
        }
      }

    \protected \lemma rdistr {x y z : ExUpperReal} (x>=0 :  <= x) (y>=0 :  <= y) : (x + y) * z = x * z + y * z
      => ExUpperRealSemigroup.*-comm *> ldistr x>=0 y>=0 *> pmap2 (+) ExUpperRealSemigroup.*-comm ExUpperRealSemigroup.*-comm

    \protected \lemma zro_*-left {x : ExUpperReal} (xb : x.IsBounded) :  * x =  \elim xb
      | inP (q,x<q) => <=-antisymmetric (\lam {b} b>0 => *_U_<=.
        \have | p1 => RatField.zro<ide <∘l join-right
              | p2 => RatField.<_*_positive_positive b>0 (RatField.finv>0 p1)
        \in inP (b RatField.* RatField.finv (q ∨ ), p2, p2, q ∨ , U_<= x<q join-left, p1, =_<= $ *-assoc *> pmap (b RatField.*) (RatField.finv-left $ RatField.>_/= p1) *> RatField.ide-right)) (\lam {b} b>0*x => \case *_U. b>0*x \with {
          | inP (a,_,a>0,c,x<c,c>0,ac<b) => RatField.<_*_positive_positive a>0 c>0 <∘ ac<b
        })

    \protected \lemma zro_*-right {x : ExUpperReal} (xb : x.IsBounded) : x *  = 
      => ExUpperRealSemigroup.*-comm *> zro_*-left xb

    \lemma *n_*_<= {n : Nat} {x : ExUpperReal} (x>=0 :  <= x) : n AddMonoid.*n x <= n * x \elim n
      |  => *_>=0
      | suc n => <=_+ (*n_*_<= x>=0) <=-refl <=∘ =_<= (pmap (_ +) (inv $ ide-left x>=0) *> inv (rdistr (<=-rat. fromNat_>=0) $ <=-less zro<ide) *> pmap (`* x) +-rat)

    \lemma *n_* {n : Nat} {x : ExUpperReal} (x>=0 :  <= x) (xb : x.IsBounded) : n AddMonoid.*n x = n * x \elim n
      |  => inv (zro_*-left xb)
      | suc n => pmap2 (+) (*n_* x>=0 xb) (inv $ ide-left x>=0) *> inv (rdistr (<=-rat. fromNat_>=0) $ <=-less zro<ide) *> pmap (`* x) +-rat

    \lemma <_*-positive {x y : ExUpperReal} (x>0 :  < x) (y>0 :  < y) :  < x * y \elim x>0, y>0
      | inP (a,a>0,a<=x), inP (b,b>0,b<=y) => inP (a RatField.* b, RatField.<_*_positive_positive a>0 b>0, transport (`<= _) (*-rat (<=-less a>0) (<=-less b>0)) $ ExUpperRealSemigroup.<=_* a<=x b<=y)

    \open ExUpperRealAbMonoid

    \sfunc div-lb {a : Rat} {b : ExUpperReal} (a>0 :  < a) (b>0 :  < b) : \Sigma (c : ExUpperReal) ( < c) (a * c <= b)
      => (ExUpperReal.fromRat (RatField.finv a) * b,
          <_*-positive (<-rat. $ RatField.finv>0 $ <-rat. a>0) b>0,
          \have a>0 => <-rat. a>0
          \in =_<= $ inv ExUpperRealSemigroup.*-assoc *> pmap (`* b) (ExUpperReal.*-rat (<=-less a>0) (<=-less $ RatField.finv>0 a>0) *> pmap ExUpperReal.fromRat (RatField.finv-right $ RatField.>_/= a>0)) *> ExUpperRealSemigroup.ide-left (<=-less b>0))

    \lemma div-lb-rat {a : Rat} {b : ExUpperReal} (a>0 :  < a) (b>0 :  < b) : ∃ (c : Rat) ( RatField.< c) (a * c <= b)
      => \case div-lb a>0 b>0 \with {
        | (c, inP (d,d>0,d<=c), ac<=b) => inP (d, d>0, <=_* <=-refl d<=c <=∘ ac<=b)
      }

    \lemma finv_<=-rotate-right {a : Rat} (a>0 :  RatField.< a) {b c : ExUpperReal} (p : RatField.finv a * b <= c) : b <= a * c
      => ide-left_<= <=∘ =_<= (pmap (`* b) (inv (*-rat (<=-less a>0) (RatField.finv>=0 $ <=-less a>0) *> pmap fromRat (RatField.finv-right $ RatField.>_/= a>0))) *> ExUpperRealSemigroup.*-assoc) <=∘ <=_* <=-refl p

    \lemma finv_<-rotate-right {a : Rat} (a>0 :  RatField.< a) {b c : ExUpperReal} (p : RatField.finv a * b < c) : b < a * c \elim p
      | inP (q,a1b<q,q<=c) => inP (a RatField.* q, \case *_U. a1b<q \with {
        | inP (d,a1<d,d>0,e,b<e,e>0,de<q) => U-closed b<e $ transport (_ RatField.<) *-comm (RatField.<_rotate-right d>0 $ transport (RatField.`< _) *-comm de<q) <∘ <_*_positive-left (RatField.finv_<-left a>0 a1<d) (*_>=0 a1b<q)
      }, transport (`<= _) (*-rat (<=-less a>0) (<=-less $ *_>=0 a1b<q)) $ <=_* <=-refl q<=c)

    \lemma finv_<-rotate-left {a : Rat} (a>0 :  RatField.< a) {b c : ExUpperReal} (c>0 :  < c) (p : b < a * c) : RatField.finv a * b < c
      => transport (_ <) (inv ExUpperRealSemigroup.*-assoc *> pmap (`* c) (*-rat (<=-less $ RatField.finv>0 a>0) (<=-less a>0) *> pmap fromRat (RatField.finv-left $ RatField.>_/= a>0)) *> ide-left (<=-less c>0)) $ <_*-right (RatField.finv>0 a>0) p $ <_*-positive (<-rat. a>0) c>0

    \func pow (x : ExUpperReal) (n : Nat) : ExUpperReal \elim n
      |  => 
      | suc n => pow x n * x

    \lemma rat-pow {x : Rat} (x>=0 :  RatField.<= x) {n : Nat} : pow x n = ExUpperReal.fromRat (RatField.pow x n) \elim n
      |  => idp
      | suc n => pmap (`* x) (rat-pow x>=0) *> *-rat (RatField.pow>=0 x>=0) x>=0

    \lemma pow_<= {x y : ExUpperReal} (x<=y : x <= y) {n : Nat} : pow x n <= pow y n \elim n
      |  => <=-refl
      | suc n => <=_* (pow_<= x<=y) x<=y

    \lemma pow_>=0 {x : ExUpperReal} {n : Nat} :  <= pow x n \elim n
      |  => <=-less zro<ide
      | suc n => *_>=0

    \lemma square_<= {x : ExUpperReal} {q : Rat} (q>=0 :  RatField.<= q) (xx<=qq : x * x <= q RatField.* q) : x <= q
      => \lam {r} q<r => \case *_U. $ xx<=qq $ RatField.<=_*_positive-right q>=0 (<=-less q<r) <∘r RatField.<_*_positive-left q<r (q>=0 <∘r q<r) \with {
        | inP (a,x<a,a>0,b,x<b,b>0,ab<rr) => \case LinearOrder.dec<_<= a r, LinearOrder.dec<_<= b r \with {
          | inl a<r, _ => U-closed x<a a<r
          | _, inl b<r => U-closed x<b b<r
          | inr r<=a, inr r<=b => absurd $ <-irreflexive $ RatField.<=_*_positive-left r<=a (q>=0 <=∘ <=-less q<r) <∘r RatField.<=_*_positive-right (<=-less a>0) r<=b <∘r ab<rr
        }
      }

    \lemma square<=1 {x : ExUpperReal} (xx<=1 : x * x <= ) : x <= 
      => square_<= rat_<=-dec xx<=1

    \lemma square-bound-div {x : ExUpperReal} (xb : x.IsBounded) {q : Rat} (q>=0 :  RatField.<= q) (xx<=qx : x * x <= q * x) : x <= q \elim xb
      | inP (B,x<B) => \case LinearOrder.dec<_<= q B \with {
        | inl q<B => \lam {r} q<r =>
          \have (n,np) => rat_<1_pow-bound {ratio  } idp {RatField.finv (B - q) RatField.* (r - q)} $ RatField.<_*_positive_positive (RatField.finv>0 $ RatField.to>0 q<B) (RatField.to>0 q<r)
          \in aux {x} {q} {q>=0} {xx<=qx} (<=-less $ RatField.to>0 q<B) (ExUpperReal.<_<= $ transport x.U linarith x<B) n $ linarith $ rewrite RatField.finv_finv in RatField.<_rotate-left (RatField.finv>0 $ RatField.to>0 q<B) np
        | inr B<=q => ExUpperReal.<_<= (x.U_<= x<B B<=q)
      }
      \where \private {
        \lemma step {e : Rat} (e>=0 :  RatField.<= e) (x<=q+e : x <= q RatField.+ e) : x <= q RatField.+ e RatField.* ratio  
          => square_<= (RatField.<=_+ q>=0 $ <=_*-positive e>=0 rat_<=-dec) $ xx<=qx <=∘ <=_* <=-refl x<=q+e <=∘ transportInv (`<= _) (*-rat q>=0 $ <=_+ q>=0 e>=0) (<=-rat. $ transport2 (RatField.<=) {_} {_} {q RatField.* q RatField.+ q RatField.* e RatField.* ratio   RatField.*  RatField.+ (e RatField.* e) RatField.* ratio   RatField.* ratio  } (inv RatField.ldistr) equation.cRing $ linarith (RatField.<=_*_positive_positive e>=0 e>=0))

        \lemma aux {e : Rat} (e>=0 :  RatField.<= e) (x<=q+e : x <= q RatField.+ e) (n : Nat) : x <= q RatField.+ e RatField.* RatField.pow (ratio  ) n \elim n
          |  => transportInv (x <= q RatField.+ __) RatField.ide-right x<=q+e
          | suc n => rewriteI RatField.*-assoc $ step (<=_*-positive e>=0 $ RatField.pow>=0 rat_<=-dec) (aux e>=0 x<=q+e n)
      }

    \lemma *n-bounded {n : Nat} {x : ExUpperReal} (xb : x.IsBounded) : (n ExUpperRealAbMonoid.*n x).IsBounded \elim xb
      | inP (q,x<q) => \case NatSemiring.decideEq n  \with {
        | yes n=0 => inP $ (, rewrite n=0 idp)
        | no n/=0 => inP (n RatField.* q, (*n_U n/=0). $ inP (q,x<q,<=-refl))
      }
  }

\record UpperReal \extends ExUpperReal {
  | U-inh : ∃ U

  \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))
    }

  \lemma U-inh_>0 : ∃ (q : U) ( < q)
    => \case U-inh \with {
      | inP (q,Uq) => inP (q ∨ , U_<= Uq join-left, zro<ide <∘l join-right)
    }

  \type IsLocated : \Prop
    => \Pi {a b : Rat} -> a < b -> ∀ {c : U} (a < c) || U b
} \where {
  \use \coerce fromRat (x : Rat) : UpperReal \cowith
    | ExUpperReal => ExUpperReal.fromRat x
    | U-inh => inP (x + , linarith)

  \lemma ex-ext {x y : UpperReal} (p : x = {ExUpperReal} y) : x = y
    => ext $ pmap (ExUpperReal.U {__}) p
}

\instance UpperRealSemigroup : CSemigroup UpperReal
  | * => *
  | *-assoc => UpperReal.ex-ext $ *-ex *> pmap (ExUpperReal.`* _) *-ex *> ExUpperRealSemigroup.*-assoc *> inv (*-ex *> pmap (_ ExUpperReal.*) *-ex)
  | *-comm => UpperReal.ex-ext $ *-ex *> ExUpperRealSemigroup.*-comm *> inv *-ex
  \where {
    \sfunc \infixl  * (x y : UpperReal) : UpperReal \cowith
      | ExUpperReal => \eval x ExUpperReal.* y
      | U-inh => \case x.U-inh_>0, y.U-inh_>0 \with {
        | inP (q,x<q,q>0), inP (r,y<r,r>0) => inP (q RatField.* r + , inP (q, x<q, q>0, r, y<r, r>0, linarith))
      }

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

    \lemma *-ex {x y : UpperReal} : x * y = x ExUpperReal.* y
      => exts \lam q => ext (<->trans *_U $ <->sym ExUpperReal.*_U)
  }