{- TODO
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ordered
\import Algebra.Ring
\import Arith.Rat
\import Arith.Real
\import Arith.Real.Field
\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 Monoid(pow)
\open LinearlyOrderedSemiring
\open LinearOrder \hiding (<=, Dec)

\func rootR (n : Nat) (x : Real) (x>=0 : 0 <= x) : Real \cowith
| L a => (a < 0) || x.L (pow a n)
| L-inh => inP (-1, byLeft idp)
| L-closed {q} {q'} e q'<q => \case dec<_<= q' 0, \elim e \with {
| inl q'<0, _ => byLeft q'<0
| inr q'>=0, byLeft q<0 => absurd linarith
| inr q'>=0, byRight q^n<x => byRight $x.L_<= q^n<x$ pow_<=-monotone q'>=0 $<_<= q'<q } | L-rounded {q} => \case dec<_<= q 0, \elim __ \with { | inl q<0, _ => inP (RatField.mid q 0, byLeft$ RatField.mid<right q<0, RatField.mid>left q<0)
| inr q>=0, byLeft q<0 => absurd (q>=0 q<0)
| inr q>=0, byRight q^n<x => \case L-rounded q^n<x \with {
| inP (b,b<x,q^n<b) => \case pow-L-rounded q>=0 q^n<b \with {
| inP (r,q<r,r^n<b) => inP (r, byRight $L-closed b<x r^n<b, q<r) } } } | U b => x.U (pow b n) | U-inh => {?} | U-closed => {?} | U-rounded => {?} | LU-disjoint => {?} | LU-located => {?} | LU-focus => {?} \where { \sfunc pow>0-rounded {b : Rat} {n : Nat} (n/=0 : n /= 0) (b>0 : 0 < b) : \Sigma (a : Rat) (0 < a) (pow a n < b) => ((b ∧ 1) * ratio 1 2, RatField.<_*_positive_positive (<_meet-univ b>0 idp) idp, transport2 (<) (inv CMonoid.pow_*-comm) ide-right$
<_*_positive-right {_} {pow (b ∧ 1) n} {pow (ratio 1 2) n} {1} (RatField.pow>0 $<_meet-univ b>0 idp) (pow<=id (<_<=$ later idp) (<_<= $later idp) n/=0 <∘r idp) <∘l {_} {_} {_} {b * 1} transport2 (<=) (inv ide-right) (inv ide-right) (pow<=id (meet-univ (<_<= b>0)$ <_<= zro<ide) meet-right n/=0 <=∘ meet-left))

\lemma pow-L-rounded {a b : Rat} (a>=0 : 0 <= a) {n : Nat} (a^n<b : pow a n < b) : ∃ (a' : Rat) (a < a') (pow a' n < b) \elim n
| 0 => inP (a + 1, linarith, a^n<b)
| suc n => \case dec<_<= 0 a \with {
| inl a>0 => \case (RealField.*_positive-U (RatField.pow>0 a>0) a>0).1 $rewrite RealField.*-rat a^n<b \with { | inP (b',a',a^n<b',a<a',b'a'<b) => \case pow-L-rounded a>=0 a^n<b' \with { | inP (a'',a<a'',a''^n<b') => \have a'a''>0 : 0 < a' ∧ a'' => <_meet-univ (a>=0 <∘r a<a') (a>=0 <∘r a<a'') \in inP (a' ∧ a'', <_meet-univ a<a' a<a'', <=_*_positive-right (<_<=$ RatField.pow>0 $a'a''>0) meet-left <∘r <=_*_positive-left (pow_<=-monotone (<_<= a'a''>0) meet-right <=∘ <_<= a''^n<b') (<_<=$ a>=0 <∘r a<a') <∘r b'a'<b)
}
}
| inr a<=0 =>
\have | a=0 : a = 0 => <=-antisymmetric a<=0 a>=0
| r => pow>0-rounded {b} {suc n} (\case __) \$ rewrite (a=0,Algebra.Ring.Ring.zro_*-right) in a^n<b
\in inP (r.1, rewrite a=0 r.2, r.3)
}
}
-}