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 m <′′ n -> ¬ (n ≤′′ m) m ¬ (m <′′ n × n ≤′′ m) ¬[m m ≤′′ n -> n ≤′′ m -> m ≡ n ≤′′-antisym ≤′′-refl _ = ≡-refl ≤′′-antisym (≤′′-step 1+m≤n) n≤m = ⊥-elim (¬[m 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)