Rat

\import Algebra.Domain.Euclidean
\import Algebra.Field
\import Algebra.Group
\import Algebra.Monoid
\import Algebra.Monoid.GCD
\import Algebra.Monoid.Sub
\import Algebra.Ordered
\import Algebra.Ring
\import Algebra.Ring.Localization
\import Algebra.Ring.Localization.Field
\import Algebra.Semiring
\import Arith.Fin
\import Arith.Int
\import Arith.Nat
\import Data.Bool
\import Data.Or
\import Function.Meta ($)
\import Logic
\import Meta
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Set
\open EuclideanSemiringData
\open Monoid(LDiv)

\data Rat
  | rat (nom : Int) (denom : Nat) (\property denom/=0 : denom /= 0) (\property reduced : gcd (iabs nom) denom = 1)
  \where {
    \use \coerce fromInt (x : Int)
      => rat x 1 (\case __) (natUnit (reduce*gcd-right (iabs x) 1))

    \func AltRat : CRing => LocRing subset
      \where \func subset : SubMonoid => localization-isOrderedField.positiveSubset IntRing

    \lemma eta {x : Rat} : x = rat (ratNom x) (ratDenom x) (ratDenom/=0 x) (ratReduced x) \elim x
      | rat _ _ _ _ => idp

    \lemma ext {x y : Rat} (p : ratNom x = ratNom y) (q : ratDenom x = ratDenom y) : x = y \elim x, y
      | rat nom1 denom1 denom1/=0 reduced1, rat nom2 denom2 denom2/=0 reduced2 =>
          path (\lam i => rat (p i) (q i) (prop-dpi _ _ _ i) (prop-dpi (\lam j => gcd (iabs (p j)) (q j) = 1) _ _ i))
  }

\func ratNom (x : Rat) : Int
  | rat n _ _ _ => n

\func ratDenom (x : Rat) : Nat
  | rat _ d _ _ => d

\func ratDenom/=0 (x : Rat) : ratDenom x /= 0
  | rat _ _ p _ => p

\func ratReduced (x : Rat) : gcd (iabs (ratNom x)) (ratDenom x) = 1
  | rat _ _ _ p => p

\open Rat(AltRat)

\func makeRat (nom : Int) (denom : Nat) (denom/=0 : denom /= 0) : Rat \elim denom
  | 1 => nom
  | denom => makeRat' nom denom denom/=0
  \where {
    \func makeRat' (nom : Int) (denom : Nat) (denom/=0 : denom /= 0) : Rat \elim nom
      | 0 => rat 0 1 (\case __) idp
      | pos (suc _ \as nom) =>
        \let! (a,b) => reduce nom denom
        \in rat a b (reduce2/=0 nom denom denom/=0) (gcd_reduced nom denom denom/=0)
      | neg (suc _ \as nom) =>
        \let! (a,b) => reduce nom denom
        \in rat (neg a) b (reduce2/=0 nom denom denom/=0) (gcd_reduced nom denom denom/=0)

    \lemma simp {nom : Int} {denom : Nat} {denom/=0 : denom /= 0} : makeRat nom denom denom/=0 = makeRat' nom denom denom/=0 \elim denom
      | 0 => idp
      | 1 => \case \elim nom \with {
        | 0 => idp
        | pos (suc n) => Rat.ext (pmap (\lam x => pos (suc x)) (inv ide-left)) idp
        | neg (suc n) => Rat.ext (pmap (\lam x => neg (suc x)) (inv ide-left)) idp
      }
      | suc (suc _) => idp

    \lemma reduce1/=0 {a b : Nat} : Not ((reduce (suc a) b).1 = 0)
      => NatSemiring.ldiv/=0 (\case __) (LDiv.swap (GCD.gcd|val1 {gcd-isGCD (suc a) b}))

    \lemma reduce2/=0 (a b : Nat) (b/=0 : Not (b = 0)) : Not ((reduce a b).2 = 0)
      => \lam b'=0 => b/=0 (inv (reduce*gcd-right _ _) *> pmap (`* gcd _ _) b'=0 *> zro_*-left)

    \lemma div0 {x : Nat} (a|b : LDiv 0 x) : x = 0
      => inv a|b.inv-right *> zro_*-left

    \lemma gcd_reduced (a b : Nat) (b/=0 : Not (b = 0)) : gcd (reduce a b).1 (reduce a b).2 = 1
      => nat_gcd-isUnique (gcd-isGCD (reduce a b).1 (reduce a b).2) $ GCD.reduce {gcd-isGCD a b} $ NatSemiring.cancel_*-left \lam gcd=0 => b/=0 $ div0 $ transport (LDiv __ b) gcd=0 $ GCD.gcd|val2 {gcd-isGCD a b}

    \lemma signum_nom {nom : Int} {denom : Nat} {denom/=0 : Not (denom = 0)} : signum (ratNom (makeRat nom denom denom/=0)) = signum nom
      => mcases {makeRat} \with {
        | 1, _ => idp
        | denom1, denom/=0' => \case \elim nom \with {
          | 0 => idp
          | pos (suc _) => signum.signum_pos reduce1/=0
          | neg (suc _) => signum.signum_neg reduce1/=0
        }
      }

    \lemma eta {x : Rat} : makeRat (ratNom x) (ratDenom x) (ratDenom/=0 x) = x
      => rat_alt-inj rat_alt_makeRat.alt
  }

\func rat_alt (x : Rat) : AltRat
  => in~ (ratNom x, ratDenom x, signum.signum_pos (ratDenom/=0 x))

\lemma rat_alt-inj {x y : Rat} (p : rat_alt x = rat_alt y) : x = y
  => \have | x0*y1=y0*x1 => loc_unequals_domain (localization-isOrderedField.positiveSubset IntRing) (\lam x c x=0 => \case rewrite x=0 c) p
           | |x0|*y1=|y0|*x1 => inv iabs_* *> pmap iabs x0*y1=y0*x1 *> iabs_*
           | sgn[x0]=sgn[y0] => inv ide-right *> inv (pmap (_ *) (signum.signum_pos $ ratDenom/=0 y)) *> inv signum.*-comm *> pmap signum x0*y1=y0*x1 *> signum.*-comm *> pmap (_ *) (signum.signum_pos $ ratDenom/=0 x) *> ide-right
     \in Rat.ext (signum_iabs_eq sgn[x0]=sgn[y0] $
        natAssociates-areEqual (nat_gcd_*_div (\new LDiv { | inv => ratDenom y | inv-right => |x0|*y1=|y0|*x1 *> *-comm }) (ratReduced x))
                               (nat_gcd_*_div (\new LDiv { | inv => ratDenom x | inv-right => inv |x0|*y1=|y0|*x1 *> *-comm }) (ratReduced y))) $
        natAssociates-areEqual (nat_gcd_*_div (\new LDiv { | inv => iabs (ratNom y) | inv-right => *-comm *> inv |x0|*y1=|y0|*x1 }) (nat_gcd-comm *> ratReduced x))
                               (nat_gcd_*_div (\new LDiv { | inv => iabs (ratNom x) | inv-right => *-comm *> |x0|*y1=|y0|*x1 }) (nat_gcd-comm *> ratReduced y))

\lemma rat_alt_makeRat {nom : Int} {denom : Nat} {denom/=0 : Not (denom = 0)} {p : signum (pos denom) = 1} : rat_alt (makeRat nom denom denom/=0) = in~ (nom, denom, p)
  => LocRing.equals1 aux
  \where {
    \lemma aux {a : Int} {b : Nat} {b/=0 : Not (b = 0)} : ratNom (makeRat a b b/=0) * b = a * ratDenom (makeRat a b b/=0) \elim b
      | 0 => absurd (b/=0 idp)
      | 1 => idp
      | suc (suc _) \as b => \case \elim a \with {
        | 0 => IntRing.zro_*-left {b}
        | pos (suc n) => unfold_let (pmap pos (aux2 b/=0))
        | neg (suc n) => unfold_let (IntRing.negative_*-left {(reduce (suc n) b).1} *> pmap neg (aux2 b/=0))
      }

    \lemma aux2 {a b : Nat} (b/=0 : Not (b = 0)) : (reduce a b).1 * b = a * (reduce a b).2
      => NatSemiring.cancel_*-left (Semiring.ldiv/=0 b/=0 (GCD.gcd|val2 {gcd-isGCD a b}))
          (inv *-assoc *> pmap (`* b) (LDiv.inv-right {GCD.gcd|val1 {gcd-isGCD a b}}) *> pmap (a *) (inv (LDiv.inv-right {GCD.gcd|val2 {gcd-isGCD a b}}) *> *-comm) *> inv *-assoc *> *-comm)

    \lemma alt : rat_alt (makeRat nom denom denom/=0) = in~ (nom, denom, signum.signum_pos denom/=0)
      => rat_alt_makeRat
  }

\instance RatField : DiscreteOrderedField Rat
  | zro => rat 0 1 (\case __) idp
  | + (x y : Rat) : Rat \with {
    | rat xNom 1 xDenom/=0 _, rat yNom 1 yDenom/=0 _ => makeRat (xNom IntRing.+ yNom) 1 (\case __)
    | rat xNom xDenom xDenom/=0 _, rat yNom yDenom yDenom/=0 _ => makeRat (xNom IntRing.* yDenom IntRing.+ yNom IntRing.* xDenom) (xDenom Nat.* yDenom) (productNonZero xDenom/=0 yDenom/=0)
  }
  | zro-left {x} => rat_alt-inj $ +_alt *> AltRat.zro-left {rat_alt x}
  | +-assoc {x} {y} {z} => rat_alt-inj $ +_alt *> pmap (AltRat.`+ rat_alt z) +_alt *> AltRat.+-assoc {rat_alt x} {rat_alt y} {rat_alt z} *> inv (+_alt *> pmap (rat_alt x AltRat.+) +_alt)
  | +-comm {x} {y} => rat_alt-inj $ +_alt *> AltRat.+-comm {rat_alt x} {rat_alt y} *> inv +_alt
  | ide => rat 1 1 (\case __) idp
  | * (x y : Rat) : Rat \with {
    | rat xNom xDenom xDenom/=0 _, rat yNom yDenom yDenom/=0 _ => makeRat (xNom IntRing.* yNom) (xDenom Nat.* yDenom) (productNonZero xDenom/=0 yDenom/=0)
  }
  | ide-left {x} => rat_alt-inj $ *_alt *> AltRat.ide-left {rat_alt x}
  | *-assoc {x} {y} {z} => rat_alt-inj $ *_alt *> pmap (__ AltRat.* rat_alt z) *_alt *> AltRat.*-assoc {rat_alt x} {rat_alt y} {rat_alt z} *> inv (*_alt *> pmap (rat_alt x AltRat.*) *_alt)
  | ldistr {x} {y} {z} => rat_alt-inj $ *_alt *> pmap (rat_alt x AltRat.*) +_alt *> AltRat.ldistr {rat_alt x} {rat_alt y} {rat_alt z} *> inv (+_alt *> pmap2 (AltRat.+) *_alt *_alt)
  | negative (x : Rat) : Rat \with {
    rat xNom xDenom xDenom/=0 xReduced => rat (IntRing.negative xNom) xDenom xDenom/=0 (rewrite iabs.negative-comm xReduced)
  }
  | negative-left {x} => rat_alt-inj $ +_alt *> pmap (AltRat.`+ rat_alt x) negative_alt *> AltRat.negative-left {rat_alt x} *> LocRing.equals1 idp
  | *-comm {x} {y} => rat_alt-inj $ *_alt *> AltRat.*-comm {rat_alt x} {rat_alt y} *> inv *_alt
  | isPos x => isPos (ratNom x)
  | zro/>0 => \case __
  | positive_+ => mcases {+} \with {
    | rat xNom 1 xDenom/=0 reduced, rat yNom 1 yDenom/=0 reduced1 => positive_+
    | rat xNom xDenom xDenom/=0 reduced, rat yNom yDenom yDenom/=0 reduced1 => \lam x>0 y>0 => makeRat.signum_nom *> IntRing.positive_+ (IntRing.positive_* x>0 (signum.signum_pos yDenom/=0)) (IntRing.positive_* y>0 (signum.signum_pos xDenom/=0))
  }
  | ide>zro => idp
  | positive_* {x} {y} => cases (x,y) (makeRat.signum_nom *> IntRing.positive_* __ __)
  | finv (x : Rat) : Rat \with {
    | rat 0 _ _ _ => rat 0 1 (\case __) idp
    | rat (pos (suc n)) b b/=0 r => rat (pos b) (suc n) (\case __) (nat_gcd-comm *> r)
    | rat (neg (suc n)) b b/=0 r => rat (neg b) (suc n) (\case __) (nat_gcd-comm *> r)
  }
  | finv_zro => idp
  | finv-right {x} x/=0 =>
    \have t : ratNom x IntRing.* ratNom (finv x) = ratDenom x Nat.* ratDenom (finv x) => \case \elim x, \elim x/=0 \with {
      | rat 0 b _ r, x/=0 => absurd (x/=0 (rat_alt-inj (LocRing.equals1 (later simplify))))
      | rat (pos (suc n)) b b/=0 reduced, _ => pmap pos *-comm
      | rat (neg (suc n)) b b/=0 reduced, _ => pmap pos *-comm
    }
    \in rat_alt-inj $ *_alt *> LocRing.equals1 (ide-right *> t *> inv ide-left)
  | decideEq x y => \case decideEq (ratNom x) (ratNom y), decideEq (ratDenom x) (ratDenom y) \with {
    | yes p, yes q => yes (Rat.ext p q)
    | no p, _ => no \lam x=y => p $ pmap ratNom x=y
    | _, no q => no \lam x=y => q $ pmap ratDenom x=y
  }
  | #0=>eitherPosOrNeg {x} xInv =>
    \case \elim x, \elim xInv \with {
      | rat n1 d1 d1/=0 r1, (rat n2 d2 d2/=0 r2, il, _) => IntRing.#0=>eitherPosOrNeg {n1} \lam n1=0 => \case inv makeRat.simp *> (rewrite (n1=0,IntRing.zro_*-right) in il)
    }
  | natCoef n => rat n 1 (\case __) idp
  | natCoefZero => idp
  | natCoefSuc n => idp
  | meet (x y : Rat) : Rat \with {
    | rat n1 d1 _ _ \as x, rat n2 d2 _ _ \as y => \case LinearOrder.dec<_<= (n2 IntRing.* d1) (n1 IntRing.* d2) \with {
      | inl y<x => y
      | inr x<=y => x
    }
  }
  | meet-left {x} {y} => \case \elim x, \elim y \with {
    | rat n1 d1 _ r1, rat n2 d2 _ _ => mcases \with {
      | inl y<x => \lam p => <-irreflexive $ <-char-conv-aux r1 p <∘ y<x
      | inr _ => \lam p => \case rewrite (+=+', makeRat.signum_nom, IntRing.negative_*-left, IntRing.negative-right) in unfolds p
    }
  }
  | meet-right {x} {y} => \case \elim x, \elim y \with {
    | rat n1 d1 _ _, rat n2 d2 _ _ => mcases \with {
      | inl _ => \lam p => \case rewrite (+=+', makeRat.signum_nom, IntRing.negative_*-left, IntRing.negative-right) in unfolds p
      | inr x<=y => \lam p => x<=y $ rewrite (+=+', makeRat.signum_nom, IntRing.negative_*-left) in unfolds p
    }
  }
  | meet-univ {x} {y} {z} => \case \elim x, \elim y, \elim z \with {
    | rat n1 d1 _ _, rat n2 d2 _ _, rat n3 d3 _ _ => \lam p q => mcases \with {
      | inl y<x => q
      | inr x<=y => p
    }
  }
  | join (x y : Rat) : Rat \with {
    | rat n1 d1 _ _ \as x, rat n2 d2 _ _ \as y => \case LinearOrder.dec<_<= (n1 IntRing.* d2) (n2 IntRing.* d1) \with {
      | inl x<y => y
      | inr y<=x => x
    }
  }
  | join-left {x} {y} => \case \elim x, \elim y \with {
    | rat n1 d1 _ _, rat n2 d2 _ r2 => mcases \with {
      | inl x<y => \lam p => <-irreflexive $ <-char-conv-aux r2 p <∘ x<y
      | inr _ => \lam p => \case rewrite (+=+', makeRat.signum_nom, IntRing.negative_*-left, IntRing.negative-right) in unfolds p
    }
  }
  | join-right {x} {y} => \case \elim x, \elim y \with {
    | rat n1 d1 _ _, rat n2 d2 _ _ => mcases \with {
      | inl _ => \lam p => \case rewrite (+=+', makeRat.signum_nom, IntRing.negative_*-left, IntRing.negative-right) in unfolds p
      | inr x<=y => \lam p => x<=y $ rewrite (+=+', makeRat.signum_nom, IntRing.negative_*-left) in unfolds p
    }
  }
  | join-univ {x} {y} {z} => \case \elim x, \elim y, \elim z \with {
    | rat n1 d1 _ _, rat n2 d2 _ _, rat n3 d3 _ _ => \lam p q => mcases \with {
      | inl y<x => q
      | inr x<=y => p
    }
  }
  \where {
    \lemma productNonZero {n m : Nat} (n/=0 : Not (n = 0)) (m/=0 : Not (m = 0)) : Not (n Nat.* m = 0)
      => \lam p => IntDomain.#0-* {pos n} {pos m} (\lam q => n/=0 (pmap iabs q)) (\lam q => m/=0 (pmap iabs q)) (pmap pos p)

    \func \infixl 6 +' (x y : Rat) : Rat
      | rat xNom xDenom xDenom/=0 _, rat yNom yDenom yDenom/=0 _ => makeRat (xNom IntRing.* yDenom IntRing.+ yNom IntRing.* xDenom) (xDenom Nat.* yDenom) (productNonZero xDenom/=0 yDenom/=0)

    \lemma +=+' {x y : Rat} : x + y = x +' y
      => mcases {+} \with {
        | rat xNom 1 xDenom/=0 reduced, rat yNom 1 yDenom/=0 reduced1 => Rat.ext simplify idp
        | rat xNom xDenom xDenom/=0 reduced, rat yNom yDenom yDenom/=0 reduced1 => idp
      }

    \lemma +_alt {x y : Rat} : rat_alt (x + y) = rat_alt x AltRat.+ rat_alt y \elim x, y
      | rat xNom xDenom xDenom/=0 reduced, rat yNom yDenom yDenom/=0 reduced1 => rewrite +=+' rat_alt_makeRat

    \lemma *_alt {x y : Rat} : rat_alt (x * y) = rat_alt x AltRat.* rat_alt y \elim x, y
      | rat nom1 denom1 denom1/=0 reduced1, rat nom2 denom2 denom2/=0 reduced2 => rat_alt_makeRat

    \lemma negative_alt {x : Rat} : rat_alt (negative x) = AltRat.negative (rat_alt x) \elim x
      | rat nom denom denom/=0 reduced => idp

    \lemma ratNom=0 {x : Rat} (p : ratNom x = 0) : x = rat 0 1 (\case __) idp \elim x
      | rat nom denom denom/=0 reduced => Rat.ext p $ inv EuclideanSemiringData.gcd_0 *> nat_gcd-comm *> (rewrite (pmap iabs p) in reduced)

    \open Arith.Rat(RatField)

    \lemma <-char {q r : Rat} (p : ratNom q IntRing.* ratDenom r < ratNom r IntRing.* ratDenom q) : q < r \elim q, r
      | rat n1 d1 c1 r1, rat n2 d2 c2 r2 => unfolds $ rewrite (+=+', IntRing.negative_*-left) (makeRat.signum_nom *> p)

    \private \lemma <-char-conv-aux {n1 n2 : Int} {d1 d2 : Nat} {d1/=0 : d1 /= 0} {d2/=0 : d2 /= 0} (r1 : gcd (iabs n1) d1 = 1) {r2 : gcd (iabs n2) d2 = 1} (p : signum (ratNom (rat n2 d2 d2/=0 r2 + negative (rat n1 d1 d1/=0 r1))) = 1) : n1 IntRing.* d2 < n2 IntRing.* d1
      => unfold (-) (rewrite (+=+',IntRing.negative_*-left) (inv makeRat.signum_nom)) *> p

    \lemma <-char-conv {q r : Rat} (q<r : q < r) : ratNom q IntRing.* ratDenom r < ratNom r IntRing.* ratDenom q \elim q, r
      | rat n1 d1 c1 r1, rat n2 d2 c2 r2 => <-char-conv-aux r1 q<r

    \lemma <=-char {q r : Rat} (p : ratNom q IntRing.* ratDenom r <= ratNom r IntRing.* ratDenom q) : q <= r
      => \lam r<q => p (<-char-conv r<q)

    \lemma <=-char-conv {q r : Rat} (q<=r : q <= r) : ratNom q IntRing.* ratDenom r <= ratNom r IntRing.* ratDenom q
      => \lam p => q<=r (<-char p)

    \lemma suc-inv {n : Nat} : Monoid.Inv {RatField} (suc n) (finv (suc n))
      => DiscreteField.nonZero-Inv \lam p => later \case pmap ratNom p

    \func mid (a b : Rat) => (a + b) * ratio 1 2

    \lemma mid>left {a b : Rat} (p : a < b) : a < mid a b
      => LinearlyOrderedSemiring.mid_inv>left (Monoid.Inv.lmake (ratio 1 2) idp) p

    \lemma mid<right {a b : Rat} (p : a < b) : mid a b < b
      => LinearlyOrderedSemiring.mid_inv<right (Monoid.Inv.lmake (ratio 1 2) idp) p

    \lemma mid-between {a b : Rat} (p : a < b) : \Sigma (a < mid a b) (mid a b < b)
      => (mid>left p, mid<right p)
  }

\lemma fromInt_<= {x y : Int} (p : x <= y) : x <= {RatField} y
  => RatField.<=-char (simplify p)
  \where {
    \lemma conv {x y : Int} (p : x <= {RatField} y) : x <= y
      => transport2 (<=) ide-right ide-right (RatField.<=-char-conv p)
  }

\lemma fromInt_< {x y : Int} (p : x < y) : x < {RatField} y
  => RatField.<-char (simplify p)
  \where {
    \lemma conv {x y : Int} (p : x < {RatField} y) : x < y
      => transport2 (<) ide-right ide-right (RatField.<-char-conv p)
  }

\func ratio (nom : Int) (denom : Nat) : Rat \elim denom
  | 0 => 0
  | suc d \as denom => makeRat nom denom (\case __)

\instance RatDenseOrder : UnboundedDenseLinearOrder.Dec
  | LinearOrder.Dec => RatField
  | UnboundedDenseLinearOrder => RatField.denseOrder RatField.suc-inv

\func rat_floor (r : Rat) : Int
  | rat (pos n) d _ _ => n Nat.div d
  | rat (neg (suc _ \as n)) d _ _ => \case n Nat.mod d \with {
    | 0 => neg (n Nat.div d)
    | suc _ => neg (n Nat.div d) - 1
  }

\lemma rat_floor<id {r : Rat} : Rat.fromInt (rat_floor r) <= r \elim r
  | rat (pos n) d _ _ => RatField.<=-char $ pos<=pos div_*<=id
  | rat (neg (suc _ \as n)) d d/=0 c => mcases {1} {arg addPath} \with {
    | 0, p => \have d=1 => nat_gcd-isUnique (GCD.swap {div_gcd (mod_div p)}) (EuclideanSemiringData.gcd-isGCD n d) *> c
              \in Preorder.=_<= $ Rat.ext (later $ rewrite d=1 idp) (inv d=1)
    | suc _, _ => \lam c => (unfolds, rewrite RatField.+=+' in, inv makeRat.signum_nom *>, unfold) at c $
      \have | s : n Nat.- n Nat.div d * d = n Nat.mod d
                => IntRing.cancel-right (n Nat.div d * d) $ IntRing.+-assoc {n} {neg _} *> pmap (pos n +) IntRing.minus__ *> pmap pos (inv (Nat.divModProp n d) *> pmap (`+ _) *-comm *> +-comm)
            | t : n Nat.- suc (n Nat.div d) Nat.* d = n Nat.mod d Nat.- d
                => pmap (n Nat.-) (rdistr {_} {1}) *> rewrite NatSemiring.ide-left (pmap (pos n +) (IntRing.negative_+ {d} {n Nat.div d * d}) *> inv (IntRing.+-assoc {n} {neg _}) *> pmap (`- pos d) s)
      \in \case (inv (pmap signum t *> signum.signum_- {n Nat.mod d} {d} *> pmap negative (pos<pos (mod<right d/=0))) *> c : neg 1 = 1)
  }

\lemma rat_floor-univ {r : Rat} {x : Int} (x<=r : Rat.fromInt x <= r) : x <= rat_floor r \elim r, x
  | rat (pos _) _ _ _, neg (suc x) => neg<=pos
  | rat (pos n) d d/=0 _, pos x => pos<=pos $ transport (`<= _) (*_div=id d/=0) $ div-monotone $ pos<=pos.conv $ RatField.<=-char-conv x<=r
  | rat (neg (suc _ \as n)) d _ _, pos x => \case pos/<=neg (RatField.<=-char-conv x<=r)
  | rat (neg (suc n' \as n)) d d/=0 _, neg (suc x' \as x) =>
    \have t => neg<=neg.conv (RatField.<=-char-conv x<=r)
    \in mcases {1} {arg addPath} \with {
      | 0, p => neg<=neg $ transport (_ <=) (*_div=id d/=0) (div-monotone t)
      | suc u, s => neg<=neg \case LinearOrder.<=-dec (div-monotone t) \with {
        | inl t' => transport (_ <=) (*_div=id d/=0) $ <_suc_<= (NatSemiring.suc<suc t')
        | inr t' =>
          \have | w => rewrite (NatSemiring.*-comm, t' *> *_div=id d/=0, s) in Nat.divModProp n d
                | w' => transport (_ <=) w $ LinearlyOrderedSemiring.<=_+ t (<=-refl {_} {suc u})
          \in absurd $ <-irreflexive $ id<suc <∘l LinearlyOrderedSemiring.<=_+ (<=-refl {_} {n}) (suc<=suc zero<=_) <∘l w'
      }
    }

\func rat_ceiling (r : Rat) : Int
  => negative (rat_floor (negative r))

\lemma rat_ceiling>id {r : Rat} : r <= rat_ceiling r
  => transport (`<= _) RatField.negative-isInv $ RatField.negative_<= {_} {negative r} rat_floor<id

\lemma rat_ceiling-univ {r : Rat} {x : Int} (r<=x : r <= x) : rat_ceiling r <= x
  => transport (_ <=) IntRing.negative-isInv $ IntRing.negative_<= $ rat_floor-univ $ RatField.negative_<= {r} {x} r<=x

\lemma rat_<=-dec {r q : Rat} {so : So (rat_<=_Bool r q)} : r <= q
  => RatField.<=-char $ int_<=-dec {_} {_} {so}
  \where
    \func rat_<=_Bool (r q : Rat) : Bool
      => int_<=-dec.int_<=_Bool (ratNom r * ratDenom q) (ratNom q * ratDenom r)

\lemma rat_<-dec {r q : Rat} {so : So (rat_<_Bool r q)} : r < q
  => \case LinearOrder.dec<_<= r q \with {
    | inl r<q => r<q
    | inr q<=r => absurd $ <-irreflexive $ int_<-dec {_} {_} {so} <∘l RatField.<=-char-conv q<=r
  }
  \where
    \func rat_<_Bool (r q : Rat) : Bool
      => int_<=-dec.int_<=_Bool (isuc (ratNom r * ratDenom q)) (ratNom q * ratDenom r)