--- a/ordinal.agda	Thu Jul 30 17:22:34 2020 +0900
+++ b/ordinal.agda	Thu Jul 30 21:45:49 2020 +0900
@@ -220,7 +220,7 @@
      ; osuc-≡< = osuc-≡<
      ; TransFinite = TransFinite1
      ; TransFinite1 = TransFinite2
-     ; not-limit-p = not-limit
+     ; Oprev-p  = Oprev-p 
    } ;
    isNext = record {
         x<nx = x<nx 
@@ -245,9 +245,12 @@
              lemma3 : {n l : Nat} → (Suc (Suc n) ≤ Suc l) → l ≤ n → ⊥
              lemma3   (s≤s sn≤l) (s≤s l≤n) = lemma3 sn≤l l≤n
 
-     not-limit : (x : Ordinal) → Dec (¬ ((y : Ordinal) → ¬ (x ≡ osuc y)))
-     not-limit (ordinal lv (Φ lv)) = no (λ not → not (λ y () ))
-     not-limit (ordinal lv (OSuc lv ox)) = yes (λ not → not (ordinal lv ox) refl )
+     open Oprev
+     Oprev-p  : (x : Ordinal) → Dec ( Oprev (Ordinal {suc n})  osuc x )
+     Oprev-p  (ordinal lv (Φ lv)) = no (λ not → lemma (oprev not) (oprev=x not) ) where
+          lemma : (x : Ordinal) → osuc x ≡ (ordinal lv (Φ lv)) → ⊥
+          lemma x ()
+     Oprev-p  (ordinal lv (OSuc lv ox)) = yes record { oprev = ordinal lv ox ; oprev=x = refl }
      ord1 : Set (suc n)
      ord1 = Ordinal {suc n}
      TransFinite1 : { ψ : ord1  → Set (suc n) }