--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/nat.agda	Fri Aug 02 12:17:10 2019 +0900
@@ -0,0 +1,40 @@
+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<y) (s≤s y<x) = nat-<> x<y y<x
+
+nat-<≡ : { x : Nat } → x < x → ⊥
+nat-<≡  (s≤s lt) = nat-<≡ lt
+
+nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥
+nat-≡< refl lt = nat-<≡ lt
+
+¬a≤a : {la : Nat} → Suc la ≤ la → ⊥
+¬a≤a  (s≤s lt) = ¬a≤a  lt
+
+a<sa : {la : Nat} → la < Suc la 
+a<sa {Zero} = s≤s z≤n
+a<sa {Suc la} = s≤s a<sa 
+
+=→¬< : {x : Nat  } → ¬ ( x < x )
+=→¬< {Zero} ()
+=→¬< {Suc x} (s≤s lt) = =→¬< lt
+
+>→¬< : {x y : Nat  } → (x < y ) → ¬ ( y < x )
+>→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
+
+<-∨ : { x y : Nat } → x < Suc y → ( (x ≡ y ) ∨ (x < y) )
+<-∨ {Zero} {Zero} (s≤s z≤n) = case1 refl
+<-∨ {Zero} {Suc y} (s≤s lt) = case2 (s≤s z≤n)
+<-∨ {Suc x} {Zero} (s≤s ())
+<-∨ {Suc x} {Suc y} (s≤s lt) with <-∨ {x} {y} lt
+<-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq)
+<-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1)
+