module nat where open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) open import Data.Empty open import Relation.Nullary open import Relation.Binary.PropositionalEquality open import logic nat-<> : { x y : Nat } → x < y → y < x → ⊥ nat-<> (s≤s x x→¬< : {x y : Nat } → (x < y ) → ¬ ( y < x ) >→¬< (s≤s x→¬< x