Andrew Sneap, November 2021

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan renaming (_+_ to _βˆ”_)

open import Naturals.Properties
open import Notation.Order
open import UF.Base
open import UF.Subsingletons

open import Integers.Addition renaming (_+_ to _β„€+_)
open import Integers.Type
open import Integers.Multiplication renaming (_*_ to _β„€*_)
open import Integers.Order
open import Naturals.Multiplication renaming (_*_ to _β„•*_)
open import Rationals.Fractions
open import Rationals.FractionsOperations

module Rationals.FractionsOrder where

_𝔽≀_ _𝔽β‰₯_ : 𝔽 β†’ 𝔽 β†’ 𝓀₀ Μ‡
(x , a) 𝔽≀ (y , b) = x β„€* pos (succ b) ≀ y β„€* pos (succ a)
p 𝔽β‰₯ q = q 𝔽≀ p

𝔽≀-is-prop : (p q : 𝔽) β†’ is-prop (p 𝔽≀ q)
𝔽≀-is-prop (x , a) (y , b) = ℀≀-is-prop (x β„€* pos (succ b)) (y β„€* pos (succ a))

_𝔽<_ _𝔽>_ : 𝔽 β†’ 𝔽 β†’ 𝓀₀ Μ‡
(x , a) 𝔽< (y , b) = x β„€* pos (succ b) < y β„€* pos (succ a)
p 𝔽> q = q 𝔽< p

𝔽<-coarser-than-≀ : (p q : 𝔽) β†’ p 𝔽< q β†’ p 𝔽≀ q
𝔽<-coarser-than-≀ (x , a) (y , b) l = Ξ³
 where
  Ξ³ : (x , a) 𝔽≀ (y , b)
  Ξ³ = <-is-≀ (x β„€* pos (succ b)) (y β„€* pos (succ a)) l

𝔽<-is-prop : (p q : 𝔽) β†’ is-prop (p 𝔽< q)
𝔽<-is-prop (x , a) (y , b) = β„€<-is-prop (x β„€* pos (succ b)) (y β„€* pos (succ a))

𝔽<-trans : (p q r : 𝔽) β†’ p 𝔽< q β†’ q 𝔽< r β†’ p 𝔽< r
𝔽<-trans (x , a) (y , b) (z , c) Ξ± Ξ² = Ξ³
 where
  a' = pos (succ a)
  b' = pos (succ b)
  c' = pos (succ c)

  I : x β„€* c' β„€* b' < z β„€* a' β„€* b'
  I = β„€<-trans (x β„€* c' β„€* b') (y β„€* a' β„€* c') (z β„€* a' β„€* b') i ii
   where
    i : x β„€* c' β„€* b' < y β„€* a' β„€* c'
    i = transport (_< y β„€* a' β„€* c') Ο• ΞΈ
     where
      Ο• : x β„€* b' β„€* c' ＝ x β„€* c' β„€* b'
      Ο• = β„€-mult-rearrangement x b' c'

      ΞΈ : x β„€* b' β„€* c' < y β„€* a' β„€* c'
      ΞΈ = positive-multiplication-preserves-order (x β„€* b') (y β„€* a') c' ⋆ Ξ±

    ii : y β„€* a' β„€* c' < z β„€* a' β„€* b'
    ii = transportβ‚‚ _<_ γ₁ Ξ³β‚‚ γ₃
     where
      γ₁ : y β„€* c' β„€* a' ＝ y β„€* a' β„€* c'
      γ₁ = β„€-mult-rearrangement y c' a'

      Ξ³β‚‚ : z β„€* b' β„€* a' ＝ z β„€* a' β„€* b'
      Ξ³β‚‚ = β„€-mult-rearrangement z b' a'

      γ₃ : y β„€* c' β„€* a' < z β„€* b' β„€* a'
      γ₃ = positive-multiplication-preserves-order (y β„€* c') (z β„€* b') a' ⋆ Ξ²

  Ξ³ : x β„€* c' < z β„€* a'
  Ξ³ = ordering-right-cancellable (x β„€* c') (z β„€* a') b' ⋆ I

𝔽<-addition-preserves-order : (p q r : 𝔽) β†’ p 𝔽< q β†’ p + r 𝔽< q + r
𝔽<-addition-preserves-order (x , a) (y , b) (z , c) (n , e)
 = pred (succ c β„•* succ c β„•* succ n) , III
 where
  a' = pos (succ a)
  b' = pos (succ b)
  c' = pos (succ c)
  n' = pos (succ n)

  sa = succ a
  sb = succ b
  sn = succ n
  sc = succ c

  I : Β¬ (sc β„•* sc β„•* sn ＝ 0)
  I Ξ± = positive-not-zero n (mult-left-cancellable sn 0 c ii)
   where
    i : sc β„•* (sc β„•* sn) ＝ sc β„•* (sc β„•* 0)
    i = sc β„•* (sc β„•* sn) ＝⟨ mult-associativity sc sc sn ⁻¹      ⟩
        sc β„•* sc β„•* sn   ＝⟨ Ξ±                                   ⟩
        0                ＝⟨ zero-right-base sc ⁻¹               ⟩
        sc β„•* 0          ＝⟨ ap (sc β„•*_) (zero-right-base sc ⁻¹) ⟩
        sc β„•* (sc β„•* 0)  ∎

    ii : sc β„•* sn ＝ sc β„•* 0
    ii = mult-left-cancellable (sc β„•* sn) (sc β„•* 0) c i

  II : succβ„€ (pos (pred (sc β„•* sc β„•* sn))) ＝ c' β„€* c' β„€* n'
  II = succβ„€ (pos (pred (sc β„•* sc β„•* sn))) ＝⟨ refl ⟩
      pos (succ (pred (sc β„•* sc β„•* sn)))   ＝⟨ i    ⟩
      pos (sc β„•* sc β„•* sn)                 ＝⟨ ii   ⟩
      pos (sc β„•* sc) β„€* pos sn             ＝⟨ iii  ⟩
      pos (sc) β„€* pos (sc) β„€* pos sn       ＝⟨ refl ⟩
      c' β„€* c' β„€* n'                       ∎
   where
    i   = ap pos (succ-pred' (sc β„•* sc β„•* sn) I)
    ii  = pos-multiplication-equiv-to-β„• (sc β„•* sc) sn ⁻¹
    iii = ap (_β„€* pos sn) (pos-multiplication-equiv-to-β„• sc sc ⁻¹)

  III : succβ„€ ((x β„€* c' β„€+ z β„€* a') β„€* pos (succ (pred (sb β„•* sc)))) β„€+ pos (pred (sc β„•* sc β„•* sn))
      ＝ (y β„€* c' β„€+ z β„€* b') β„€* pos (succ (pred (sa β„•* sc)))
  III = succβ„€ ((x β„€* c' β„€+ z β„€* a') β„€* pos (succ (pred (sb β„•* sc)))) β„€+ pos (pred (sc β„•* sc β„•* sn)) ＝⟨ i     ⟩
      succβ„€ ((x β„€* c' β„€+ z β„€* a') β„€* pos (succ (pred (sb β„•* sc))) β„€+ pos (pred (sc β„•* sc β„•* sn)))   ＝⟨ ii    ⟩
      (x β„€* c' β„€+ z β„€* a') β„€* pos (succ (pred (sb β„•* sc))) β„€+ succβ„€ (pos (pred (sc β„•* sc β„•* sn)))   ＝⟨ iii   ⟩
      (x β„€* c' β„€+ z β„€* a') β„€* pos (succ (pred (sb β„•* sc))) β„€+ c' β„€* c' β„€* n'                        ＝⟨ iv    ⟩
      (x β„€* c' β„€+ z β„€* a') β„€* (b' β„€* c') β„€+ c' β„€* c' β„€* n'                                          ＝⟨ v     ⟩
      x β„€* c' β„€* (b' β„€* c') β„€+ z β„€* a' β„€* (b' β„€* c') β„€+ c' β„€* c' β„€* n'                              ＝⟨ vi    ⟩
      x β„€* c' β„€* (b' β„€* c') β„€+ (z β„€* a' β„€* (b' β„€* c') β„€+ c' β„€* c' β„€* n')                            ＝⟨ vii   ⟩
      x β„€* c' β„€* (b' β„€* c') β„€+ (c' β„€* c' β„€* n' β„€+ z β„€* a' β„€* (b' β„€* c'))                            ＝⟨ viii  ⟩
      x β„€* c' β„€* (b' β„€* c') β„€+ c' β„€* c' β„€* n' β„€+ z β„€* a' β„€* (b' β„€* c')                              ＝⟨ ix    ⟩
      x β„€* (b' β„€* c') β„€* c' β„€+ n' β„€* (c' β„€* c') β„€+ z β„€* a' β„€* (b' β„€* c')                            ＝⟨ xi    ⟩
      x β„€* b' β„€* c' β„€* c' β„€+ n' β„€* (c' β„€* c') β„€+ z β„€* a' β„€* (b' β„€* c')                              ＝⟨ xii   ⟩
      x β„€* b' β„€* (c' β„€* c') β„€+ n' β„€* (c' β„€* c') β„€+ z β„€* a' β„€* (b' β„€* c')                            ＝⟨ xiii  ⟩
      (x β„€* b' β„€+ n') β„€* (c' β„€* c') β„€+ z β„€* a' β„€* (b' β„€* c')                                        ＝⟨ xiv   ⟩
      (x β„€* b' β„€+ n') β„€* c' β„€* c' β„€+ z β„€* a' β„€* (b' β„€* c')                                          ＝⟨ xv    ⟩
      (succβ„€ (x β„€* b' β„€+ pos n)) β„€* c' β„€* c' β„€+ z β„€* a' β„€* (b' β„€* c')                               ＝⟨ xvi   ⟩
      (succβ„€ (x β„€* b') β„€+ pos n) β„€* c' β„€* c' β„€+ z β„€* a' β„€* (b' β„€* c')                               ＝⟨ xvii  ⟩
      y β„€* a' β„€* c' β„€* c' β„€+ z β„€* a' β„€* (b' β„€* c')                                                  ＝⟨ xviii ⟩
      y β„€* c' β„€* a' β„€* c' β„€+ z β„€* (a' β„€* (b' β„€* c'))                                                ＝⟨ xix   ⟩
      y β„€* c' β„€* (a' β„€* c') β„€+ z β„€* (b' β„€* (a' β„€* c'))                                              ＝⟨ xx    ⟩
      y β„€* c' β„€* (a' β„€* c') β„€+ z β„€* b' β„€* (a' β„€* c')                                                ＝⟨ xxi   ⟩
      (y β„€* c' β„€+ z β„€* b') β„€* (pos (sa) β„€* pos (sc))                                                ＝⟨ xxii  ⟩
      (y β„€* c' β„€+ z β„€* b') β„€* pos (succ (pred (sa β„•* sc)))                                          ∎
   where
    i     = β„€-left-succ ((x β„€* c' β„€+ z β„€* a') β„€* pos (succ (pred (sb β„•* sc)))) (pos (pred (sc β„•* sc β„•* sn)))
    ii    = β„€-right-succ ((x β„€* c' β„€+ z β„€* a') β„€* pos (succ (pred (sb β„•* sc)))) (pos (pred (sc β„•* sc β„•* sn))) ⁻¹
    iii   = ap ((x β„€* c' β„€+ z β„€* a') β„€* pos (succ (pred (sb β„•* sc))) β„€+_) II
    iv    = ap (Ξ» - β†’ ((x β„€* c' β„€+ z β„€* a') β„€* -) β„€+  c' β„€* c' β„€* n') (denom-setup b c)
    v     = ap (Ξ» - β†’ - β„€+ c' β„€* c' β„€* n') (distributivity-mult-over-β„€ (x β„€* c') (z β„€* a') (b' β„€* c'))
    vi    = β„€+-assoc ( x β„€* c' β„€* (b' β„€* c')) (z β„€* a' β„€* (b' β„€* c')) (c' β„€* c' β„€* n')
    vii   = ap (x β„€* c' β„€* (b' β„€* c') β„€+_) (β„€+-comm (z β„€* a' β„€* (b' β„€* c')) (c' β„€* c' β„€* n'))
    viii  = β„€+-assoc (x β„€* c' β„€* (b' β„€* c')) (c' β„€* c' β„€* n') (z β„€* a' β„€* (b' β„€* c')) ⁻¹
    ix    = apβ‚‚ (Ξ» Ξ± Ξ² β†’ Ξ± β„€+ Ξ² β„€+ z β„€* a' β„€* (b' β„€* c')) (β„€-mult-rearrangement x c' (b' β„€* c')) (β„€*-comm (c' β„€* c') n')
    xi    = ap (Ξ» - β†’ - β„€* c'  β„€+ n' β„€* (c' β„€* c') β„€+ z β„€* a' β„€* (b' β„€* c')) (β„€*-assoc x b' c' ⁻¹)
    xii   = ap (Ξ» - β†’ - β„€+ n' β„€* (c' β„€* c') β„€+ z β„€* a' β„€* (b' β„€* c')) (β„€*-assoc (x β„€* b') c' c')
    xiii  = ap (Ξ» - β†’ - β„€+ z β„€* a' β„€* (b' β„€* c')) (distributivity-mult-over-β„€ ( x β„€* b') n' (c' β„€* c') ⁻¹)
    xiv   = ap (Ξ» - β†’ - β„€+ z β„€* a' β„€* (b' β„€* c') ) (β„€*-assoc ((x β„€* b' β„€+ n')) c' c' ⁻¹)
    xv    = ap (Ξ» - β†’ - β„€* c' β„€* c' β„€+ z β„€* a' β„€* (b' β„€* c')) (β„€-right-succ (x β„€* b') (pos n))
    xvi   = ap (Ξ» - β†’ - β„€* c' β„€* c' β„€+ z β„€* a' β„€* (b' β„€* c')) (β„€-left-succ (x β„€* b') (pos n) ⁻¹)
    xvii  = ap (Ξ» - β†’ - β„€* c' β„€* c' β„€+ z β„€* a' β„€* (b' β„€* c')) e
    xviii = apβ‚‚ (Ξ» Ξ± Ξ² β†’ Ξ± β„€* c' β„€+ Ξ²) (β„€-mult-rearrangement y a' c') (β„€*-assoc z a' (b' β„€* c'))
    xix   = apβ‚‚ (Ξ» Ξ± Ξ² β†’ Ξ± β„€+ z β„€* Ξ²) (β„€*-assoc (y β„€* c') a' c') (β„€-mult-rearrangement''' a' b' c')
    xx    = ap (Ξ» - β†’ y β„€* c' β„€* (a' β„€* c') β„€+ -) (β„€*-assoc z b' (a' β„€* c') ⁻¹)
    xxi   = distributivity-mult-over-β„€ (y β„€* c') (z β„€* b') (a' β„€* c') ⁻¹
    xxii  = ap (Ξ» - β†’ (y β„€* c' β„€+ z β„€* b') β„€* -) (denom-setup a c ⁻¹)

𝔽<-adding : (p q r s : 𝔽) β†’ p 𝔽< q β†’ r 𝔽< s β†’ p + r 𝔽< q + s
𝔽<-adding p q r s l₁ lβ‚‚ = 𝔽<-trans (p + r) (q + r) (q + s) I III
 where
  I : (p + r) 𝔽< (q + r)
  I = 𝔽<-addition-preserves-order p q r l₁

  II : (r + q) 𝔽< (s + q)
  II = 𝔽<-addition-preserves-order r s q lβ‚‚

  III : (q + r) 𝔽< (q + s)
  III = transportβ‚‚ _𝔽<_ (𝔽+-comm r q) (𝔽+-comm s q) II

𝔽<-adding-zero : (p q : 𝔽)
               β†’ (pos 0 , 0) 𝔽< p
               β†’ (pos 0 , 0) 𝔽< q
               β†’ (pos 0 , 0) 𝔽< (p + q)
𝔽<-adding-zero p q l₁ lβ‚‚ = 𝔽<-adding (pos 0 , 0) p (pos 0 , 0) q l₁ lβ‚‚

𝔽-pos-multiplication-preserves-order : (p q : 𝔽)
                                     β†’ (pos 0 , 0) 𝔽< p
                                     β†’ (pos 0 , 0) 𝔽< q
                                     β†’ (pos 0 , 0) 𝔽< (p * q)
𝔽-pos-multiplication-preserves-order (x , a) (y , b) (c , e₁) (d , eβ‚‚)
 = pred (succ c β„•* succ d) , I
 where
  α : pos (succ c) ＝ x
  α = pos (succ c)                            ＝⟨ i    ⟩
      pos 0 β„€+ pos (succ c)                   ＝⟨ refl ⟩
      pos 0 β„€+ succβ„€ (pos c)                  ＝⟨ ii   ⟩
      succβ„€ (pos 0 β„€+ pos c)                  ＝⟨ iii  ⟩
      succβ„€ (pos 0) β„€+ pos c                  ＝⟨ iv   ⟩
      succβ„€ (pos 0 β„€* pos (succ a)) β„€+ pos c  ＝⟨ e₁   ⟩
      x                                       ∎
   where
    i   = β„€-zero-left-neutral (pos (succ c)) ⁻¹
    ii  = β„€-right-succ (pos 0) (pos c)
    iii = β„€-left-succ (pos 0) (pos c) ⁻¹
    iv  = ap (Ξ» - β†’ succβ„€ - β„€+ pos c) (β„€-zero-left-base (pos (succ a)) ⁻¹)

  β : pos (succ d) ＝ y
  β = pos (succ d)                           ＝⟨ i    ⟩
      pos 0 β„€+ pos (succ d)                  ＝⟨ refl ⟩
      pos 0 β„€+ succβ„€ (pos d)                 ＝⟨ ii   ⟩
      succβ„€ (pos 0 β„€+ pos d)                 ＝⟨ iii  ⟩
      succβ„€ (pos 0) β„€+ pos d                 ＝⟨ iv   ⟩
      succβ„€ (pos 0 β„€* pos (succ b)) β„€+ pos d ＝⟨ eβ‚‚   ⟩
      y                                      ∎
   where
    i   = β„€-zero-left-neutral (pos (succ d)) ⁻¹
    ii  = β„€-right-succ (pos 0) (pos d)
    iii = β„€-left-succ (pos 0) (pos d) ⁻¹
    iv  = ap (Ξ» - β†’ succβ„€ - β„€+ pos d) (β„€-zero-left-base (pos (succ b)) ⁻¹)

  I : succβ„€ (pos 0 β„€* pos (succ (pred (succ a β„•* succ b))))
       β„€+ pos (pred (succ c β„•* succ d))
    ＝ x β„€* y β„€* pos 1
  I = succβ„€ (pos 0 β„€* pos (succ (pred (succ a β„•* succ b))))
       β„€+ pos (pred (succ c β„•* succ d))                     ＝⟨ i    ⟩
      succβ„€ (pos 0) β„€+ pos (pred (succ c β„•* succ d))        ＝⟨ ii   ⟩
      succβ„€ (pos 0 β„€+ pos (pred (succ c β„•* succ d)))        ＝⟨ iii  ⟩
      succβ„€ (pos (pred (succ c β„•* succ d)))                 ＝⟨ refl ⟩
      pos (succ (pred (succ c β„•* succ d)))                  ＝⟨ iv   ⟩
      pos (succ c β„•* succ d)                                ＝⟨ v    ⟩
      pos (succ c) β„€* pos (succ d)                          ＝⟨ vi   ⟩
      x β„€* y                                                ＝⟨ vii  ⟩
      x β„€* y β„€* pos 1                                       ∎
    where
     iβ‚β‚š : pos 0 β„€* pos (succ (pred (succ a β„•* succ b))) ＝ pos 0
     iβ‚β‚š = β„€-zero-left-base (pos (succ (pred (succ a β„•* succ b))))
     ivβ‚β‚š : Β¬ (succ c β„•* succ d ＝ 0)
     ivβ‚β‚š = β„•-positive-multiplication-not-zero c d

     i   = ap (Ξ» - β†’ succβ„€ - β„€+  pos (pred (succ c β„•* succ d))) iβ‚β‚š
     ii  = β„€-left-succ (pos 0) (pos (pred (succ c β„•* succ d)))
     iii = ap succβ„€ (β„€-zero-left-neutral (pos (pred (succ c β„•* succ d))))
     iv  = ap pos (succ-pred' (succ c β„•* succ d) ivβ‚β‚š)
     v   = pos-multiplication-equiv-to-β„• (succ c) (succ d) ⁻¹
     vi  = apβ‚‚ _β„€*_ Ξ± Ξ²
     vii = β„€-mult-right-id (x β„€* y)

𝔽≀-pos-multiplication-preserves-order : (p q : 𝔽)
                                      β†’ (pos 0 , 0) 𝔽≀ p
                                      β†’ (pos 0 , 0) 𝔽≀ q
                                      β†’ (pos 0 , 0) 𝔽≀ (p * q)
𝔽≀-pos-multiplication-preserves-order (x , a) (y , b) (c , e₁) (d , eβ‚‚)
 = c β„•* d , I
 where
  a' = pos (succ a)
  c' = pos c
  d' = pos d

  I : pos 0 β„€* pos (succ (pred (succ a β„•* succ b))) β„€+ pos (c β„•* d)
    ＝ x β„€* y β„€* pos 1
  I = pos 0 β„€* pos (succ (pred (succ a β„•* succ b))) β„€+ pos (c β„•* d) ＝⟨ i    ⟩
      pos 0 β„€+ pos (c β„•* d)                                         ＝⟨ ii   ⟩
      pos 0 β„€+ c' β„€* d'                                             ＝⟨ iii  ⟩
      c' β„€* d'                                                      ＝⟨ iv   ⟩
      (pos 0 β„€+ c') β„€* d'                                           ＝⟨ v    ⟩
      (pos 0 β„€+ c') β„€* (pos 0 β„€+ d')                                ＝⟨ vi   ⟩
      (pos 0 β„€* a' β„€+ c') β„€* (pos 0 β„€+ d')                          ＝⟨ vii  ⟩
      (pos 0 β„€* a' β„€+ c') β„€* (pos 0 β„€* pos (succ b) β„€+ d')          ＝⟨ viii ⟩
      x β„€* pos 1 β„€* (y β„€* pos 1)                                    ＝⟨ ix   ⟩
      x β„€* y β„€* pos 1                                               ∎
       where
        iβ‚β‚š = β„€-zero-left-base (pos (succ (pred (succ a β„•* succ b))))
        viiiβ‚β‚š = β„€-zero-left-base (pos (succ b)) ⁻¹

        i    = ap (_β„€+ pos (c β„•* d)) iβ‚β‚š
        ii   = ap (pos 0 β„€+_) (pos-multiplication-equiv-to-β„• c d ⁻¹)
        iii  = β„€-zero-left-neutral (c' β„€* d')
        iv   = ap (_β„€* d') (β„€-zero-left-neutral c' ⁻¹)
        v    = ap ((pos 0 β„€+ c') β„€*_) (β„€-zero-left-neutral d' ⁻¹)
        vi   = ap (Ξ» z β†’ (z β„€+ c') β„€* (pos 0 β„€+ d')) (β„€-zero-left-base a' ⁻¹)
        vii  = ap (Ξ» z β†’ (pos 0 β„€* a' β„€+ c') β„€* (z β„€+ d')) viiiβ‚β‚š
        viii = apβ‚‚ _β„€*_ e₁ eβ‚‚
        ix   = ap (_β„€* (y β„€* pos 1)) (β„€-mult-right-id x ⁻¹)

0𝔽≀1 : (pos 0 , 0) 𝔽≀ (pos 1 , 0)
0𝔽≀1 = 1 , refl

1𝔽≀1 : (pos 1 , 0) 𝔽≀ (pos 1 , 0)
1𝔽≀1 = 0 , refl

2/3𝔽≀1 : (pos 2 , 2) 𝔽≀ (pos 1 , 0)
2/3𝔽≀1 = 1 , refl

negative-not-greater-than-zero : (x a : β„•) β†’ Β¬ ((pos 0 , 0) 𝔽< (negsucc x , a))
negative-not-greater-than-zero x a (n , l) = negsucc-not-pos Ξ³
 where
  Ξ³ : negsucc x β„€* pos 1 ＝ pos (succ n)
  Ξ³ = negsucc x β„€* pos 1                      ＝⟨ l ⁻¹ ⟩
      succβ„€ (pos 0 β„€* pos (succ a)) β„€+ pos n  ＝⟨ i    ⟩
      succβ„€ (pos 0 β„€* pos (succ a) β„€+ pos n)  ＝⟨ ii   ⟩
      pos 0 β„€* pos (succ a) β„€+ succβ„€ (pos n)  ＝⟨ iii  ⟩
      pos 0 β„€+ pos (succ n)                   ＝⟨ iv   ⟩
      pos (succ n)                            ∎
   where
    i   = β„€-left-succ (pos 0 β„€* pos (succ a)) (pos n)
    ii  = β„€-right-succ (pos 0 β„€* pos (succ a)) (pos n) ⁻¹
    iii = ap (_β„€+ pos (succ n)) (β„€-zero-left-base (pos (succ a)))
    iv  = β„€-zero-left-neutral (pos (succ n))

positive-order-flip : (m n a b : β„•)
                    β†’ ((pos (succ m)) , a) 𝔽< ((pos (succ n)) , b)
                    β†’ ((pos (succ a)) , m) 𝔽> ((pos (succ b)) , n)
positive-order-flip m n a b l = transportβ‚‚ _<_ I II l
 where
  I : pos (succ m) β„€* pos (succ b) ＝ pos (succ b) β„€* pos (succ m)
  I = β„€*-comm (pos (succ m)) (pos (succ b))

  II : pos (succ n) β„€* pos (succ a) ＝ pos (succ a) β„€* pos (succ n)
  II = β„€*-comm (pos (succ n)) (pos (succ a))

\end{code}