--- a/ordinal.agda	Sun Jul 12 12:32:42 2020 +0900
+++ b/ordinal.agda	Sun Jul 12 19:55:37 2020 +0900
@@ -226,10 +226,19 @@
   } where
      next : Ordinal {suc n} → Ordinal {suc n}
      next (ordinal lv ord) = ordinal (Suc lv) (Φ (Suc lv))
-     next-limit : {y : Ordinal} → (y o< next y) ∧ ((x : Ordinal) → x o< next y → osuc x o< next y)
-     next-limit {y} = record { proj1 = case1 a<sa ; proj2 = lemma } where
+     next-limit : {y : Ordinal} → (y o< next y) ∧ ((x : Ordinal) → x o< next y → osuc x o< next y) ∧
+        ( (x : Ordinal) → y o< x → x o< next y →  ¬ ((z : Ordinal) → ¬ (x ≡ osuc z)  ))
+     next-limit {y} = record { proj1 = case1 a<sa ; proj2 = record { proj1 = lemma ; proj2 = lemma2 } } where
          lemma :  (x : Ordinal) → x o< next y → osuc x o< next y
          lemma x (case1 lt) = case1 lt
+         lemma2 : (x : Ordinal) → y o< x → x o< next y → ¬ ((z : Ordinal) → ¬ x ≡ osuc z)
+         lemma2 (ordinal Zero (Φ 0)) (case2 ()) (case1 (s≤s z≤n)) not
+         lemma2 (ordinal Zero (OSuc 0 dx)) (case2 Φ<) (case1 (s≤s z≤n)) not = not _ refl
+         lemma2 (ordinal Zero (OSuc 0 dx)) (case2 (s< x)) (case1 (s≤s z≤n)) not = not _ refl
+         lemma2 (ordinal (Suc lx) (OSuc (Suc lx) ox)) y<x (case1 (s≤s (s≤s lt))) not = not _ refl
+         lemma2 (ordinal (Suc lx) (Φ (Suc lx))) (case1 x) (case1 (s≤s (s≤s lt))) not = lemma3 x lt where
+             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 )