--- a/ordinal.agda	Thu Aug 01 15:38:08 2019 +0900
+++ b/ordinal.agda	Fri Aug 02 12:17:10 2019 +0900
@@ -7,6 +7,8 @@
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
 open import Data.Empty
 open import  Relation.Binary.PropositionalEquality
+open import  logic
+open import  nat
 
 data OrdinalD {n : Level} :  (lv : Nat) → Set n where
    Φ : (lv : Nat) → OrdinalD  lv
@@ -100,34 +102,6 @@
 osucc {n} {ox} {oy} (case2 x) with d<→lv x
 ... | refl = case2 (s< x)
 
-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 < 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)
-
 case12-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord x d< ord y → ⊥
 case12-⊥ {x} {y} lt1 lt2 with d<→lv lt2
 ... | refl = nat-≡< refl lt1
@@ -344,11 +318,11 @@
       lemma0 : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal lx (Φ lx) → ψ (ordinal ly oy)
       lemma0 ly oy lt = proj2 ( TransFinite1 lx (Φ lx) ) (ordinal ly oy) lt
       lemma : (ly : Nat) (oy : OrdinalD ly ) → ordinal ly oy  o< ordinal (Suc lx) (Φ (Suc lx)) → ψ (ordinal ly oy)
-      lemma lx1 ox1 (case1 lt) with <-∨ lt
-      lemma lx (Φ lx) (case1 lt) | case1 refl = proj1 ( TransFinite1 lx (Φ lx) )
-      lemma lx (OSuc lx ox1) (case1 lt) | case1 refl = caseOSuc lx ox1 ( lemma lx ox1 (case1 a<sa)) 
-      lemma lx (Φ lx) (case1 lt) | case2 (s≤s lt1) = lemma0  lx (Φ lx) (case1 (s≤s lt1))
-      lemma lx1 (OSuc lx1 ox1) (case1 lt) | case2 lt1 = caseOSuc lx1 ox1 ( lemma lx1 ox1 (case1 (<-trans lt1 a<sa ))) 
+      lemma lx1 ox1            (case1 lt) with <-∨ lt
+      lemma lx (Φ lx)          (case1 lt) | case1 refl = proj1 ( TransFinite1 lx (Φ lx) )
+      lemma lx (Φ lx)          (case1 lt) | case2 (s≤s lt1) = lemma0  lx (Φ lx) (case1 (s≤s lt1))
+      lemma lx (OSuc lx ox1)   (case1 lt) | case1 refl = caseOSuc lx ox1  ( lemma lx ox1 (case1 a<sa)) 
+      lemma lx1 (OSuc lx1 ox1) (case1 lt) | case2 lt1  = caseOSuc lx1 ox1 ( lemma lx1 ox1 (case1 (<-trans lt1 a<sa ))) 
   TransFinite1 lx (OSuc lx ox)  = record { proj1 = caseOSuc lx ox (proj1 (TransFinite1 lx ox )) ; proj2 = proj2 (TransFinite1 lx ox )}
 
 -- we cannot prove this in intutionistic logic