module DownwardLeq where

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

open import Data.Sum
open import Data.Product
open import Data.Nat
open import Data.Nat.Properties using (n≤m+n; n≤1+n; ¬i+1+j≤i)
open import Data.Empty

data _≤′′_ : ℕ -> ℕ -> Set where
  ≤′′-refl : forall {n} -> n ≤′′ n
  ≤′′-step : forall {m n} -> suc m ≤′′ n -> m ≤′′ n

_<′′_ :  ℕ -> ℕ -> Set
m <′′ n = suc m ≤′′ n

m≤n⇒m≤1+n : forall {m n} -> m ≤′′ n -> m ≤′′ (suc n)
m≤n⇒m≤1+n ≤′′-refl = ≤′′-step ≤′′-refl
m≤n⇒m≤1+n (≤′′-step 1+m≤n) = ≤′′-step (m≤n⇒m≤1+n 1+m≤n)

0≤′′1+n : forall {n} -> 0 ≤′′ suc n
0≤′′1+n {zero} = ≤′′-step ≤′′-refl 
0≤′′1+n {suc n} = m≤n⇒m≤1+n 0≤′′1+n

1≤′′1+n : forall {n} -> 1 ≤′′ suc n
1≤′′1+n {zero} = ≤′′-refl 
1≤′′1+n {suc n} = m≤n⇒m≤1+n 1≤′′1+n

n<′′1+n : forall {n} -> n <′′ suc n
n<′′1+n = ≤′′-refl 

≤′′-suc : forall {m n} -> m ≤′′ n -> suc m ≤′′ suc n 
≤′′-suc ≤′′-refl = ≤′′-refl
≤′′-suc {m} {n} (≤′′-step 1+m≤n) = m≤n⇒m≤1+n 1+m≤n 

_≤′′?_ : forall m n -> m ≤′′ n ⊎ n <′′ m
zero ≤′′? zero = inj₁ ≤′′-refl
zero ≤′′? suc n = inj₁ 0≤′′1+n
suc m ≤′′? zero = inj₂ 1≤′′1+n 
suc m ≤′′? suc n with m ≤′′? n
... | inj₁ m≤n = inj₁ (≤′′-suc m≤n)
... | inj₂ 1+n≤m = inj₂ (≤′′-suc 1+n≤m)

≤′′⇒≤ : forall {m n} -> m ≤′′ n -> m ≤ n
≤′′⇒≤ ≤′′-refl = n≤m+n zero _
≤′′⇒≤ (≤′′-step 1+m≤n) = ≤-trans (n≤1+n _) (≤′′⇒≤ 1+m≤n) 
  where ≤-trans : forall {m n k} -> m ≤ n -> n ≤ k -> m ≤ k
        ≤-trans = IsPreorder.trans (IsPartialOrder.isPreorder (Poset.isPartialOrder poset))

¬1+n≤n : forall {n} -> ¬ (suc n ≤′′ n) 
¬1+n≤n 1+n≤n = aux (≤′′⇒≤ 1+n≤n)
  where aux :  forall {n} -> ¬ (suc n ≤ n) 
        aux {zero} ()
        aux {suc n} 2+n≤1+n = aux {n} (≤-pred 2+n≤1+n) 

m<n⇒¬n≤m : forall {m n} -> m <′′ n -> ¬ (n ≤′′ m) 
m<n⇒¬n≤m {m} .{suc m} ≤′′-refl 1+m≤m = ¬1+n≤n 1+m≤m 
m<n⇒¬n≤m {m} {n} (≤′′-step 1+m<n) n≤m = m<n⇒¬n≤m 1+m<n (m≤n⇒m≤1+n n≤m)

¬[m<n∧n≤m] : forall {m n} -> ¬ (m <′′ n × n ≤′′ m) 
¬[m<n∧n≤m] (m<n , n≤m) = m<n⇒¬n≤m m<n n≤m

≤′′-antisym : forall {m n} ->  m ≤′′ n -> n ≤′′ m -> m ≡ n
≤′′-antisym ≤′′-refl _ = ≡-refl
≤′′-antisym (≤′′-step 1+m≤n) n≤m = ⊥-elim (¬[m<n∧n≤m] (1+m≤n , n≤m))  

≤′′-trans : forall {m n k} -> m ≤′′ n -> n ≤′′ k -> m ≤′′ k
≤′′-trans ≤′′-refl m≤k = m≤k
≤′′-trans (≤′′-step 1+m≤n) n≤k = ≤′′-step (≤′′-trans 1+m≤n n≤k)