```{-# OPTIONS --type-in-type
#-}

open import NeilPrelude

module StrictPosReal where

--------------------------------------------------------

infix  3  _<ℜ⁺_ _≤ℜ⁺_ _≥ℜ⁺_ _>ℜ⁺_

postulate ℜ⁺ : Set
postulate ı⁺ : ℜ⁺
postulate halfℜ⁺ : ℜ⁺ → ℜ⁺
postulate _<ℜ⁺_ : Rel ℜ⁺
postulate <ℜ⁺-trich : Trichotomous _<ℜ⁺_
postulate <ℜ⁺-trans : Transitive _<ℜ⁺_

--------------------------------------------------------

Δ : Set
Δ = ℜ⁺

--------------------------------------------------------

import StrictTotalOrder
module STOℜ⁺ = StrictTotalOrder _<ℜ⁺_ <ℜ⁺-trans <ℜ⁺-trich
open STOℜ⁺

Compareℜ⁺ : Rel ℜ⁺
Compareℜ⁺ = OrdCompare

CompareLeqℜ⁺ : Rel ℜ⁺
CompareLeqℜ⁺ = OrdCompareLeq

CompareGeqℜ⁺ : Rel ℜ⁺
CompareGeqℜ⁺ = OrdCompareGeq

compareℜ⁺ : (x y : ℜ⁺) → Compareℜ⁺ x y
compareℜ⁺ = compare

compareLeqℜ⁺ : (x y : ℜ⁺) → CompareLeqℜ⁺ x y
compareLeqℜ⁺ = compareLeq

compareGeqℜ⁺ : (x y : ℜ⁺) → CompareGeqℜ⁺ x y
compareGeqℜ⁺ = compareGeq

_>ℜ⁺_ : Rel ℜ⁺
_>ℜ⁺_ = _>_

_≤ℜ⁺_ : Rel ℜ⁺
_≤ℜ⁺_ = _≤_

_≥ℜ⁺_ : Rel ℜ⁺
_≥ℜ⁺_ = _≥_

<ℜ⁺-irreflexive : Irreflexive _<ℜ⁺_
<ℜ⁺-irreflexive = irreflex

<ℜ⁺-asym : Asymmetric _<ℜ⁺_
<ℜ⁺-asym = asym

≤ℜ⁺-antisym : Antisymmetric _≤ℜ⁺_
≤ℜ⁺-antisym = antisymmetric

≤ℜ⁺-refl : Reflexive _≤ℜ⁺_
≤ℜ⁺-refl = reflexive

≤ℜ⁺-trans : Transitive _≤ℜ⁺_
≤ℜ⁺-trans = ≤-trans

<≤ℜ⁺-trans : Trans _<ℜ⁺_ _≤ℜ⁺_ _<ℜ⁺_
<≤ℜ⁺-trans = <≤-trans

≤<ℜ⁺-trans : Trans _≤ℜ⁺_ _<ℜ⁺_ _<ℜ⁺_
≤<ℜ⁺-trans = ≤<-trans

<≤ℜ⁺-asym : {x y : ℜ⁺} → x <ℜ⁺ y → Not (y ≤ℜ⁺ x)
<≤ℜ⁺-asym = <≤-asym

≤<ℜ⁺-asym : {x y : ℜ⁺} → x ≤ℜ⁺ y → Not (y <ℜ⁺ x)
≤<ℜ⁺-asym = ≤<-asym

--------------------------------------------------------

ifℜ⁺_≤_thenleq_elsemore_ : {A : Set} → (x y : ℜ⁺) → (x ≤ℜ⁺ y → A) → ((x >ℜ⁺ y) → A) → A
ifℜ⁺_≤_thenleq_elsemore_ = ifleq_≤_thenleq_elsemore_

ifℜ⁺_≥_thengeq_elseless_ : {A : Set} → (x y : ℜ⁺) → (x ≥ℜ⁺ y → A) → ((x <ℜ⁺ y) → A) → A
ifℜ⁺_≥_thengeq_elseless_ = ifgeq_≥_thengeq_elseless_

ifℜ⁺_<_thenless_elsegeq_ : {A : Set} → (x y : ℜ⁺) → (x <ℜ⁺ y → A) → ((x ≥ℜ⁺ y) → A) → A
ifℜ⁺_<_thenless_elsegeq_ = ifless_<_thenless_elsegeq_

ifℜ⁺_>_thenmore_elseleq_ : {A : Set} → (x y : ℜ⁺) → (x >ℜ⁺ y → A) → ((x ≤ℜ⁺ y) → A) → A
ifℜ⁺_>_thenmore_elseleq_ = ifmore_>_thenmore_elseleq_

--------------------------------------------------------

<ℜ⁺-subst : {x₁ y₁ x₂ y₂ : ℜ⁺} → x₁ ≡ x₂ → y₁ ≡ y₂ → x₁ <ℜ⁺ y₁ → x₂ <ℜ⁺ y₂
<ℜ⁺-subst refl refl = id

<ℜ⁺-substL : {x₁ x₂ y : ℜ⁺} → x₁ ≡ x₂ → x₁ <ℜ⁺ y → x₂ <ℜ⁺ y
<ℜ⁺-substL refl = id

<ℜ⁺-substR : {x y₁ y₂ : ℜ⁺} → y₁ ≡ y₂ → x <ℜ⁺ y₁ → x <ℜ⁺ y₂
<ℜ⁺-substR refl = id

≤ℜ⁺-subst : {x₁ y₁ x₂ y₂ : ℜ⁺} → x₁ ≡ x₂ → y₁ ≡ y₂ → x₁ ≤ℜ⁺ y₁ → x₂ ≤ℜ⁺ y₂
≤ℜ⁺-subst refl refl = id

≤ℜ⁺-substL : {x₁ x₂ y : ℜ⁺} → x₁ ≡ x₂ → x₁ ≤ℜ⁺ y → x₂ ≤ℜ⁺ y
≤ℜ⁺-substL refl = id

≤ℜ⁺-substR : {x y₁ y₂ : ℜ⁺} → y₁ ≡ y₂ → x ≤ℜ⁺ y₁ → x ≤ℜ⁺ y₂
≤ℜ⁺-substR refl = id

--------------------------------------------------------

infixl 10 _⁺+⁺_

postulate _⁺+⁺_ : ℜ⁺ → ℜ⁺ → ℜ⁺
postulate ℜ⁺-minus : (x y : ℜ⁺) → y <ℜ⁺ x → ℜ⁺

_⁺-⁺_ : (x y : ℜ⁺) → y <ℜ⁺ x → ℜ⁺
_⁺-⁺_ = ℜ⁺-minus

postulate ⁺+⁺-comm : {x y : ℜ⁺} → (x ⁺+⁺ y) ≡ (y ⁺+⁺ x)

--------------------------------------------------------

postulate lem-ℜ⁺-minus-proofirrelevence : {x y : ℜ⁺} → (p q : y <ℜ⁺ x) → (x ⁺-⁺ y) p ≡ (x ⁺-⁺ y) q

postulate ⁺+⁺-cancL : CancellativeL _⁺+⁺_

⁺+⁺-cancR : CancellativeR _⁺+⁺_
⁺+⁺-cancR eq = ⁺+⁺-cancL (trans2 ⁺+⁺-comm eq ⁺+⁺-comm)

postulate lem-ℜ⁺-+-<-cancellativeL : {x y z : ℜ⁺} → (p : x <ℜ⁺ y) → x ⁺+⁺ z <ℜ⁺ y ⁺+⁺ z

lem-ℜ⁺-+-<-cancellativeR : {x y z : ℜ⁺} → (p : y <ℜ⁺ z) → x ⁺+⁺ y <ℜ⁺ x ⁺+⁺ z
lem-ℜ⁺-+-<-cancellativeR {x} {y} {z} = <ℜ⁺-subst ⁺+⁺-comm ⁺+⁺-comm ∘ lem-ℜ⁺-+-<-cancellativeL {y} {z} {x}

postulate lem-ℜ⁺-minus-<-cancellative : {x y z : ℜ⁺} → (p : z <ℜ⁺ x) → (q : z <ℜ⁺ y) → x <ℜ⁺ y → (x ⁺-⁺ z) p <ℜ⁺ (y ⁺-⁺ z) q

lem-ℜ⁺-minus-≤-cancellative : {x y z : ℜ⁺} → (p : z <ℜ⁺ x) → (q : z <ℜ⁺ y) → x ≤ℜ⁺ y → (x ⁺-⁺ z) p ≤ℜ⁺ (y ⁺-⁺ z) q
lem-ℜ⁺-minus-≤-cancellative p q (inl lt) = inl (lem-ℜ⁺-minus-<-cancellative p q lt)
lem-ℜ⁺-minus-≤-cancellative p q (inr refl) = inr (lem-ℜ⁺-minus-proofirrelevence p q)

postulate lem-ℜ⁺-+-<-increasing : {x y : ℜ⁺} → x <ℜ⁺ (y ⁺+⁺ x)

lem-ℜ⁺-+-<-increasingR : {x y : ℜ⁺} → x <ℜ⁺ (x ⁺+⁺ y)
lem-ℜ⁺-+-<-increasingR = <ℜ⁺-substR ⁺+⁺-comm lem-ℜ⁺-+-<-increasing

lem-ℜ⁺-+-≱-increasingR : {x y : ℜ⁺} → Not (x ≥ℜ⁺ (x ⁺+⁺ y))
lem-ℜ⁺-+-≱-increasingR p = <≤ℜ⁺-asym lem-ℜ⁺-+-<-increasingR p

--------------------------------------------------------

postulate lem-ℜ⁺-x+[y-x]=y : {x y : ℜ⁺} → (p : x <ℜ⁺ y) → x ⁺+⁺ ((y ⁺-⁺ x) p) ≡ y
postulate lem-ℜ⁺-[x+y]-x=y : {x y : ℜ⁺} → (p : x <ℜ⁺ (x ⁺+⁺ y)) → ((x ⁺+⁺ y) ⁺-⁺ x) p ≡ y
postulate lem-ℜ⁺-x-y<z→x<y+z : {x y z : ℜ⁺} → (p : y <ℜ⁺ x) → ((x ⁺-⁺ y) p <ℜ⁺ z) → x <ℜ⁺ (y ⁺+⁺ z)
postulate lem-ℜ⁺-y<z-x→x+y<z : {x y z : ℜ⁺} → (p : x <ℜ⁺ z) → (y <ℜ⁺ (z ⁺-⁺ x) p) → (x ⁺+⁺ y) <ℜ⁺ z
postulate lem-ℜ⁺-x-[y+z]=[x-y]-z : {x y z : ℜ⁺} → (p : (y ⁺+⁺ z) <ℜ⁺ x) → (q : y <ℜ⁺ x) → (r : z <ℜ⁺ ((x ⁺-⁺ y) q) ) → ((x ⁺-⁺ (y ⁺+⁺ z)) p ≡ ((x ⁺-⁺ y) q ⁺-⁺ z) r)

--------------------------------------------------------

infixl 11 _⁺*⁺_

postulate _⁺*⁺_   : ℜ⁺ → ℜ⁺ → ℜ⁺

--------------------------------------------------------

_⁺<=⁺_ : ℜ⁺ → ℜ⁺ → Bool
_⁺<=⁺_ = _<='_

_⁺>=⁺_ : ℜ⁺ → ℜ⁺ → Bool
_⁺>=⁺_ = _>='_

_⁺<⁺_ : ℜ⁺ → ℜ⁺ → Bool
_⁺<⁺_ = _<'_

_⁺>⁺_ : ℜ⁺ → ℜ⁺ → Bool
_⁺>⁺_ = _>'_

----------------------------------------------------------------
```