module My.SetTheory.Nat.Order where

-- §──────────────────────────────────────────────────────────────────
-- Required modules
-- §──────────────────────────────────────────────────────────────────

import Data.Empty as DE
import Data.Nat as DN
import Data.Nat.Properties as DNP
import Data.Product as DP
import Function as F
import Relation.Binary as RB
import Relation.Binary.PropositionalEquality as RBPE

open DN using (_+_ ; _≤_ ; _<_ ; _>_ ; _<′_)
open DP using (_×_)
open F using (_$_)
open RBPE using (_≡_ ; _≢_)

import My.SetTheory.Relation.Trichotomy as MySTRT
import My.SetTheory.Nat.TvD as MySTNTVD

-- §──────────────────────────────────────────────────────────────────
-- Order respects equality
-- §──────────────────────────────────────────────────────────────────

≤-resp-≡ˡ : {n x y : DN.ℕ} → x ≡ y → n ≤ x → n ≤ y
≤-resp-≡ˡ x≡y n≤x = DTO.trans n≤x $ DTO.reflexive x≡y
  where
    module DTO = RB.DecTotalOrder DN.decTotalOrder

≤-resp-≡ʳ : {n x y : DN.ℕ} → x ≡ y → x ≤ n → y ≤ n
≤-resp-≡ʳ x≡y x≤n = DTO.trans (DTO.reflexive $ RBPE.sym x≡y) x≤n
  where
    module DTO = RB.DecTotalOrder DN.decTotalOrder

<-resp-≡ : ({n x y : DN.ℕ} → x ≡ y → n < x → n < y) ×
  ({n x y : DN.ℕ} → x ≡ y → x < n → y < n)
<-resp-≡ = STO.<-resp-≈
  where
    module STO = RB.StrictTotalOrder DNP.strictTotalOrder

<-resp-≡ˡ : {n x y : DN.ℕ} → x ≡ y → n < x → n < y
<-resp-≡ˡ = DP.proj₁ <-resp-≡

<′-resp-≡ˡ : {n x y : DN.ℕ} → x ≡ y → n <′ x → n <′ y
<′-resp-≡ˡ p q =  DNP.≤⇒≤′ $ <-resp-≡ˡ p $ DNP.≤′⇒≤ q

<-resp-≡ʳ : {n x y : DN.ℕ} → x ≡ y → x < n → y < n
<-resp-≡ʳ = DP.proj₂ <-resp-≡

<′-resp-≡ʳ : {n x y : DN.ℕ} → x ≡ y → x <′ n → y <′ n
<′-resp-≡ʳ p q = DNP.≤⇒≤′ $ <-resp-≡ʳ p $ DNP.≤′⇒≤ q

-- §──────────────────────────────────────────────────────────────────
-- Any nat is less than its sum with a positive nat.
-- §──────────────────────────────────────────────────────────────────


m<s⌈m+n⌉ : (m n : DN.ℕ) → m < DN.suc (m + n)
m<s⌈m+n⌉ m n = DN.s≤s $ DNP.m≤m+n m n

m<′s⌈m+n⌉ : (m n : DN.ℕ) → m <′ DN.suc (m + n)
m<′s⌈m+n⌉ m n = DNP.≤⇒≤′ $ m<s⌈m+n⌉ m n

-- §──────────────────────────────────────────────────────────────────
-- A nat is not equal to zero if it is at least 1, and not equal to 1
-- if it is at least 2.
-- §──────────────────────────────────────────────────────────────────

1≤n⇒n≢0 : {n : DN.ℕ} →  ≤ n → n ≢ 
1≤n⇒n≢0 {} () n≡0
1≤n⇒n≢0 {DN.suc n} 1≤n ()

2≤n⇏n≢1 : {n : DN.ℕ} →  ≤ n → n ≢ 
2≤n⇏n≢1 {n} 2≤n n≡1 = r
  where
    1<n :  < n
    1<n = 2≤n
    1≢n :  ≢ n
    1≢n = MySTRT.trichABC⇒A⇒¬B (MySTNTVD.≡-<-trich  n) 1<n
    r   : DE.⊥
    r   = 1≢n (RBPE.sym n≡1)