\import Algebra.Field
\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Ordered
\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
}
}
\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
}
}
\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 (q + m r q) (r - m r q) (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 $ <-transitive-left pr>0 rat_ceiling>id
| s : (r' - q') * (finv eps * (r - q)) < r - q
=> <-transitive-left (<_*_positive-right (r-q>0 Lq' Ur') $ <-transitive-right rat_ceiling>id $ <-transitive-right (fromInt_<= $ Preorder.=_<= $ inv $ iabs.pos_iabs c>0) (pow>id _)) 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)
}
} \where {
\open DiscreteOrderedField
\open DiscreteField
\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)) => <-transitive-right linarith (<_*_positive-left (pow>id (suc (suc n))) idp)
\use \coerce fromRat (x : Rat) : Real \cowith
| L => `< x
| L-closed s t => <-transitive t s
| L-rounded q<x => TruncP.map (isDense q<x) (\lam t => (t.1,t.3,t.2))
| U => x <
| U-closed => <-transitive
| U-rounded => isDense
| LU-disjoint q<x x<q => <-irreflexive (<-transitive q<x x<q)
| LU-focus eps eps>0 => inP (x - eps * finv 2, linarith, linarith)
}
\instance RealField : OrderedField Real
| zro => Real.fromRat 0
| + (x y : Real) : Real \cowith {
| L q => ∃ (r : x.L) (s : y.L) (q = r +' s)
| L-closed {q} {q'} (inP (r,xLr,s,yLs,q=r+s)) q'<q => inP (r - q +' q', x.L-closed xLr linarith, s, yLs, linarith)
| L-rounded {q} (inP (r,xLr,s,yLs,q=r+s)) => TruncP.map (x.L-rounded xLr) (\lam t => (q +' t.1 - r, inP (t.1,t.2,s,yLs,linarith), linarith t.3))
| U q => ∃ (r : x.U) (s : y.U) (q = r +' s)
| U-closed {q} {q'} (inP (r,xUr,s,yUs,q=r+s)) q<q' => inP (r +' q' - q, x.U-closed xUr linarith, s, yUs, linarith)
| U-rounded {q} (inP (r,xUr,s,yUs,q=r+s)) => TruncP.map (y.U-rounded yUs) (\lam t => (q - s +' t.1, inP (r,xUr,t.1,t.2,linarith), linarith t.3))
| LU-disjoint {q} (inP (r,xLr,s,yLs,q=r+s)) (inP (r',xUr',s',yUs',q=r+s')) => linarith (x.LU-less xLr xUr', y.LU-less yLs yUs')
| LU-focus eps eps>0 =>
\let | eps' => eps *' finv 2
| eps'>0 : eps' > 0 => OrderedSemiring.<_*_positive_positive eps>0 idp
\in \case x.LU-focus eps' eps'>0, y.LU-focus eps' eps'>0 \with {
| inP (a,xLa,xU[a+e']), inP (b,yLb,yU[b+e']) => inP (a +' b, inP (a,xLa,b,yLb,idp), inP (a +' eps', xU[a+e'], b +' eps', yU[b+e'], linarith))
}
}
| zro-left {x : Real} => exts (\lam q => ext (\lam (inP (r,r<0,s,xLs,q=r+s)) => x.L-closed xLs linarith, \lam xLq => TruncP.map (x.L-rounded xLq) (\lam t => (q - t.1, linarith t.3, t.1, t.2, linarith))),
\lam q => ext (\lam (inP (r,r>0,s,xUs,q=r+s)) => x.U-closed xUs linarith, \lam xUq => TruncP.map (x.U-rounded xUq) (\lam t => (q - t.1, linarith t.3, t.1, t.2, linarith))))
| +-assoc {x y z : Real} =>
\have | lr {q} {P Q R : Rat -> \Prop}
: ∃ (r : Rat) (∃ (r' : P) (s' : Q) (r = r' +' s')) (s : R) (q = r +' s) -> ∃ (r : P) (s : Rat) (∃ (r' : Q) (s' : R) (s = r' +' s')) (q = r +' s)
=> \lam (inP (r,inP (r',xUr',s',yUs',r=r'+s'),s,zUs,q=r+s)) => inP (r', xUr', s' +' s, inP (s', yUs', s, zUs, idp), q=r+s *> pmap (`+' s) r=r'+s' *> +-assoc)
| rl {q} {P Q R : Rat -> \Prop}
: ∃ (r : P) (s : Rat) (∃ (r' : Q) (s' : R) (s = r' +' s')) (q = r +' s) -> ∃ (r : Rat) (∃ (r' : P) (s' : Q) (r = r' +' s')) (s : R) (q = r +' s)
=> \lam (inP (r,Pr,s,inP (r',Qr',s',Rs',s=r'+s'),q=r+s)) => inP (r +' r', inP (r,Pr,r',Qr',idp), s', Rs', q=r+s *> pmap (r +') s=r'+s' *> inv +-assoc)
\in exts (\lam q => ext (lr, rl), \lam q => ext (lr, rl))
| +-comm =>
\have lem {q : Rat} {P Q : Rat -> \Prop} : ∃ (r : P) (s : Q) (q = r +' s) -> ∃ (s : Q) (r : P) (q = s +' r)
=> TruncP.map __ (\lam t => (t.3, t.4, t.1, t.2, t.5 *> +-comm))
\in exts (\lam q => ext (lem, lem), \lam q => ext (lem, lem))
| ide => Real.fromRat 1
| * (x y : Real) : Real \cowith {
| L q => ∃ (a : x.L) (b : x.U) (c : y.L) (d : y.U) (q < a *' c) (q < a *' d) (q < b *' c) (q < b *' d)
| L-closed {q} {q'} (inP (a,xLa,b,xUb,c,yLc,d,yUd,q<ac,q<ad,q<bc,q<bd)) q'<q => inP (a,xLa,b,xUb,c,yLc,d,yUd, <-transitive q'<q q<ac, <-transitive q'<q q<ad, <-transitive q'<q q<bc, <-transitive q'<q q<bd)
| L-rounded {q} (inP (a,xLa,b,xUb,c,yLc,d,yUd,q<ac,q<ad,q<bc,q<bd)) =>
\let | m => (a *' c) ∧ (a *' d) ∧ (b *' c) ∧ (b *' d)
| q<m => <_meet-univ (<_meet-univ (<_meet-univ q<ac q<ad) q<bc) q<bd
| mid<m => mid<right suc-inv q<m
\in inP (mid suc-inv q m, inP (a,xLa,b,xUb,c,yLc,d,yUd, <-transitive-left mid<m (meet-left <=∘ meet-left <=∘ meet-left), <-transitive-left mid<m (meet-left <=∘ meet-left <=∘ meet-right), <-transitive-left mid<m (meet-left <=∘ meet-right), <-transitive-left mid<m meet-right), mid>left suc-inv q<m)
| U q => ∃ (a : x.L) (b : x.U) (c : y.L) (d : y.U) (a *' c < q) (a *' d < q) (b *' c < q) (b *' d < q)
| U-closed {q} {q'} (inP (a,xLa,b,xUb,c,yLc,d,yUd,ac<q,ad<q,bc<q,bd<q)) q<q' => inP (a,xLa,b,xUb,c,yLc,d,yUd, <-transitive ac<q q<q', <-transitive ad<q q<q', <-transitive bc<q q<q', <-transitive bd<q q<q')
| U-rounded {q} (inP (a,xLa,b,xUb,c,yLc,d,yUd,ac<q,ad<q,bc<q,bd<q)) =>
\let | m => (a *' c) ∨ (a *' d) ∨ (b *' c) ∨ (b *' d)
| m<q => <_join-univ (<_join-univ (<_join-univ ac<q ad<q) bc<q) bd<q
| m<mid => mid>left suc-inv m<q
\in inP (mid suc-inv m q, inP (a,xLa,b,xUb,c,yLc,d,yUd, <-transitive-right (join-left <=∘ join-left <=∘ join-left) m<mid, <-transitive-right (join-right <=∘ join-left <=∘ join-left) m<mid, <-transitive-right (join-right <=∘ join-left) m<mid, <-transitive-right join-right m<mid), mid<right suc-inv m<q)
| LU-disjoint {q} (inP (a,xLa,b,xUb,c,yLc,d,yUd,q<ac,q<ad,q<bc,q<bd)) (inP (a',xLa',b',xUb',c',yLc',d',yUd',a'c'<q,a'd'<q,b'c'<q,b'd'<q)) =>
\have | d'>=0 : 0 <= d' => \case dec<_<= d' 0 \with {
| inl d'<0 => absurd $ \case dec<_<= b 0 \with {
| inl b<0 => <-irreflexive $ <-transitive (<-transitive a'c'<q q<bd) $ <-transitive (RatField.<_*_negative-right b<0 (y.LU-less yLc' yUd)) $ RatField.<_*_negative-left (x.LU-less xLa' xUb) (<-transitive (y.LU-less yLc' yUd') d'<0)
| inr b>=0 => <-irreflexive $ <-transitive (<-transitive a'd'<q q<bc) $ <-transitive-right (RatField.<=_*_positive-right b>=0 $ <=-less $ y.LU-less yLc yUd') (RatField.<_*_negative-left (x.LU-less xLa' xUb) d'<0)
}
| inr d'>=0 => d'>=0
}
| b'>=0 : 0 <= b' => \case dec<_<= b' 0 \with {
| inl b'<0 => absurd $ \case dec<_<= d 0 \with {
| inl d<0 => <-irreflexive $ <-transitive (<-transitive a'c'<q q<bd) $ <-transitive (RatField.<_*_negative-left (x.LU-less xLa' xUb) d<0) (RatField.<_*_negative-right (<-transitive (x.LU-less xLa' xUb') b'<0) (y.LU-less yLc' yUd))
| inr d>=0 => <-irreflexive $ <-transitive (<-transitive b'c'<q q<ad) $ <-transitive-right (<=_*_positive-left (<=-less $ x.LU-less xLa xUb') d>=0) (RatField.<_*_negative-right b'<0 (y.LU-less yLc' yUd))
}
| inr b'>=0 => b'>=0
}
| a<0 : a < 0 => \case dec<_<= a 0 \with {
| inl a<0 => a<0
| inr a>=0 => absurd $ <-irreflexive $ <-transitive-left (<-transitive b'd'<q q<ac) $ <=_*_positive-right a>=0 (<=-less $ y.LU-less yLc yUd') <=∘ <=_*_positive-left (<=-less $ x.LU-less xLa xUb') d'>=0
}
| d>=0 : 0 <= d => \case dec<_<= d 0 \with {
| inl d<0 => absurd $ \case dec<_<= a' 0 \with {
| inl a'<0 => <-irreflexive $ <-transitive (<-transitive a'c'<q q<bd) $ <-transitive (RatField.<_*_negative-left (x.LU-less xLa' xUb) d<0) (RatField.<_*_negative-right a'<0 (y.LU-less yLc' yUd))
| inr a'>=0 => <-irreflexive $ <-transitive (<-transitive a'd'<q q<bc) $ <-transitive-left (RatField.<_*_negative-left (x.LU-less xLa' xUb) (<-transitive (y.LU-less yLc yUd) d<0)) $ RatField.<=_*_positive-right a'>=0 $ <=-less (y.LU-less yLc yUd')
}
| inr d>=0 => d>=0
}
\in RatField.<-irreflexive $ <-transitive-left (<-transitive b'd'<q q<ad) $ RatField.<=_*_positive-left (<=-less a<0) d>=0 <=∘ simplify <=-refl <=∘ RatField.<=_*_positive-left b'>=0 d'>=0
| LU-focus eps eps>0 => {?}
}
| ide-left => {?}
| ide-right => {?}
| *-comm => {?}
| *-assoc => {?}
| ldistr => {?}
| negative (x : Real) : Real \cowith {
| L q => x.U (negative' q)
| L-closed xU-q q'<q => x.U-closed xU-q (RatField.negative_< q'<q)
| L-rounded xU-q => TruncP.map (x.U-rounded xU-q) $ \lam t => (negative' t.1, transportInv x.U negative-isInv t.2, rewriteF negative-isInv (RatField.negative_< t.3))
| U q => x.L (negative' q)
| U-closed xL-q q<q' => x.L-closed xL-q (RatField.negative_< q<q')
| U-rounded xL-q => TruncP.map (x.L-rounded xL-q) $ \lam t => (negative' t.1, transportInv x.L negative-isInv t.2, rewriteF negative-isInv (RatField.negative_< t.3))
| LU-disjoint xU-q xL-q => LU-disjoint xL-q xU-q
| LU-focus eps eps>0 => TruncP.map (x.LU-focus eps eps>0) $ \lam t => (negative' (t.1 +' eps), transportInv x.U negative-isInv t.3, transport x.L linarith t.2)
}
| negative-left {x : Real} => exts (\lam q => ext (\lam (inP (r,xU-r,s,xLs,q=r+s)) => linarith (using (Real.LU-less xLs xU-r)),
\lam q<0 => TruncP.map (x.LU-focus (negative' q) (RatField.negative_< q<0)) (\lam t => (q - t.1, transport x.U linarith t.3, t.1, t.2, linarith))),
\lam q => ext (\lam (inP (r,xL-r,s,xUs,q=r+s)) => linarith (using (Real.LU-less xL-r xUs)),
\lam q>0 => TruncP.map (x.LU-focus q q>0) (\lam t => (negative' t.1, transportInv x.L negative-isInv t.2, t.1 +' q, t.3, linarith))))
| isPos (x : Real) => x.L 0
| zro/>0 => <-irreflexive
| positive_+ x>0 y>0 => inP (0, x>0, 0, y>0, idp)
| ide>zro => idp
| <_+-comparison (x y : Real) (inP (r,xLr,s,yLs,zro=r+s)) => \case dec<_<= 0 r \with {
| inl r>0 => byLeft (x.L-closed xLr r>0)
| inr r<0 => byRight (y.L_<= yLs linarith)
}
| <_+-connectedness {x : Real} x/<0 x/>0 =>
exts (\lam q => ext (\lam xLq => \case dec<_<= q 0 \with {
| inl q<0 => q<0
| inr q>=0 => absurd $ x/<0 $ x.L_<= xLq q>=0
}, \case x.LU-located q 0 __ \with {
| byLeft xLq => xLq
| byRight xU0 => absurd (x/>0 xU0)
}), \lam q => ext (\lam xUq => \case dec<_<= 0 q \with {
| inl q>0 => q>0
| inr q<=0 => absurd $ x/>0 $ x.U_<= xUq q<=0
}, \case x.LU-located 0 q __ \with {
| byLeft xL0 => absurd (x/<0 xL0)
| byRight xUq => xUq
}))
| positive_* {x y : Real} x>0 y>0 => \case x.L-rounded x>0, x.U-inh, y.L-rounded y>0, y.U-inh \with {
| inP (a,xLa,a>0), inP (b,xUb), inP (c,yLc,c>0), inP (d,yUd) =>
\have | b>0 => x.LU-less x>0 xUb
| d>0 => y.LU-less y>0 yUd
\in inP (a,xLa,b,xUb,c,yLc,d,yUd, RatField.<_*_positive_positive a>0 c>0, RatField.<_*_positive_positive a>0 d>0, RatField.<_*_positive_positive b>0 c>0, RatField.<_*_positive_positive b>0 d>0)
}
| positive=>#0 {x : Real} x>0 => Monoid.Inv.lmake (pinv x>0) {?}
| #0=>eitherPosOrNeg {x : Real} (xInv : Monoid.Inv x) => \case propExt.conv (pmap (Real.L {__} 0) xInv.inv-right) zro<ide \with {
| inP (a,xLa,b,xUb,c,yLc,d,yUd,ac>0,ad>0,bc>0,bd>0) => \case dec<_<= a 0, dec<_<= 0 b, dec<_<= c 0 \with {
| inr a>=0, _, _ => byLeft (x.L_<= xLa a>=0)
| _, inr b<=0, _ => byRight (x.U_<= xUb b<=0)
| inl a<0, inl b>0, inl c<0 => absurd $ <-irreflexive $ <-transitive bc>0 $ RatField.<_*_positive_negative b>0 c<0
| inl a<0, inl b>0, inr c>=0 => absurd $ <-irreflexive $ <-transitive-left ac>0 $ RatField.<=_*_negative_positive (<=-less a<0) c>=0
}
}
\where {
\open AddMonoid(+ \as \infixl 6 +')
\open Monoid(* \as \infixl 7 *')
\open AddGroup(negative \as negative')
\open LinearlyOrderedSemiring
\open RatField(suc-inv)
\open AddGroup(negative-isInv)
\func pinv {x : Real} (x>0 : x.L 0) : Real \cowith
| L q => 0 < q -> ∃ (r : x.U) (q *' r < 1)
| L-closed f q'<q q'>0 => TruncP.map (f (<-transitive q'>0 q'<q)) $ \lam (r,xUr,qr<1) => (r, xUr, <-transitive (RatField.<_*_positive-left q'<q (x.LU-less x>0 xUr)) qr<1)
| L-rounded {q} f => \case trichotomy q 0 \with {
| less q<0 => inP (0, \lam c => absurd (<-irreflexive c), q<0)
| equals q=0 => TruncP.map x.U-inh $ \lam (r,xUr) =>
\have | r>0 => x.LU-less x>0 xUr
| r+1>0 : 0 < r +' 1 => linarith
\in (finv (r +' 1), \lam _ => inP (r, xUr, RatField.<_rotate-left r+1>0 $ transportInv (r <) ide-right linarith), transportInv (`< _) q=0 $ RatField.finv>0 r+1>0)
| greater q>0 =>
\have | (inP (r,xUr,qr<1)) => f q>0
| (inP (r',xUr',r'<r)) => x.U-rounded xUr
| r'/=0 => RatField.>_/= (x.LU-less x>0 xUr')
\in inP ((q *' r) *' finv r', \lam _ => inP (r', xUr', transportInv (`< 1) (*-assoc *> pmap (_ *') (RatField.finv-left r'/=0) *> ide-right) qr<1), transport (`< _) (*-assoc *> pmap (q *') (finv-right r'/=0) *> ide-right) $ RatField.<_*_positive-left (RatField.<_*_positive-right q>0 r'<r) $ RatField.finv>0 $ x.LU-less x>0 xUr')
}
| U q => ∃ (r : x.L) (1 < q *' r) (0 < q)
| U-closed (inP (r,xLr,qr>1,q>0)) q<q' => inP (r, xLr, <-transitive qr>1 $ RatField.<_*_positive-left q<q' $ \case dec<_<= 0 r \with {
| inl r>0 => r>0
| inr r<=0 => absurd $ <-irreflexive $ <-transitive qr>1 $ <-transitive-right (RatField.<=_*_positive_negative (<=-less q>0) r<=0) zro<ide
}, <-transitive q>0 q<q')
| U-rounded {q} (inP (r,xLr,qr>1,q>0)) => TruncP.map (x.L-rounded xLr) $ \lam (r',xLr',r<r') =>
\have | r>0 : 0 < r => \case dec<_<= 0 r \with {
| inl r>0 => r>0
| inr r<=0 => absurd $ <-irreflexive $ <-transitive-left (<-transitive zro<ide qr>1) $ RatField.<=_*_positive_negative (<=-less q>0) r<=0
}
| r'>0 => <-transitive r>0 r<r'
| r'/=0 => RatField.>_/= r'>0
\in (q *' r *' finv r', inP (r', xLr', transportInv (1 <) (*-assoc *> pmap (_ *') (RatField.finv-left r'/=0) *> ide-right) qr>1, RatField.<_*_positive_positive (RatField.<_*_positive_positive q>0 r>0) $ RatField.finv>0 r'>0), transport (_ <) (*-assoc *> pmap (q *') (finv-right r'/=0) *> ide-right) $ RatField.<_*_positive-left (RatField.<_*_positive-right q>0 r<r') $ RatField.finv>0 r'>0)
| LU-disjoint f (inP (s,xLs,qs>1,q>0)) => \case f q>0 \with {
| inP (r,xUr,qr<1) => <-irreflexive $ <-transitive qs>1 $ <-transitive (RatField.<_*_positive-right q>0 $ x.LU-less xLs xUr) qr<1
}
| LU-focus => {?}
}