--- a/Ordinals.agda	Mon Jul 13 13:29:38 2020 +0900
+++ b/Ordinals.agda	Mon Jul 13 13:55:46 2020 +0900
@@ -228,15 +228,21 @@
         next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (proj2 (proj2 next-limit) (next z) x<nz (ordtrans c y<nx )
            (λ w nz=ow → o<¬≡ (sym nz=ow) (proj1 (proj2 next-limit) _ (subst (λ k → w o< k ) (sym nz=ow) <-osuc ))))
 
+        osuc< : {x y : Ordinal} → osuc x ≡ y → x o< y
+        osuc< {x} {y} refl = <-osuc 
+
         nexto=n : {x y : Ordinal} → x o< next (osuc y)  → x o< next y 
         nexto=n {x} {y} x<noy = next< (proj1 (proj2 next-limit) _ (proj1 next-limit)) x<noy
 
         nexto≡ : {x : Ordinal} → next x ≡ next (osuc x)  
         nexto≡ {x} with trio< (next x) (next (osuc x) ) 
-        nexto≡ {x} | tri< a ¬b ¬c = {!!}
+        --    next x o< next (osuc x ) ->  osuc x o< next x o< next (osuc x) -> next x ≡ osuc z -> z o o< next x -> osuc z o< next x -> next x o< next x
+        nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim ((proj2 (proj2 next-limit)) _ (proj1 (proj2 next-limit) _ (proj1 next-limit) ) a
+           (λ z eq → o<¬≡ (sym eq) ((proj1 (proj2 next-limit)) _ (osuc< (sym eq)))))
         nexto≡ {x} | tri≈ ¬a b ¬c = b
+        --    next (osuc x) o< next x ->  osuc x o< next (osuc x) o< next x -> next (osuc x) ≡ osuc z -> z o o< next (osuc x) ...
         nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim ((proj2 (proj2 next-limit)) _ (ordtrans <-osuc (proj1 next-limit)) c
-           (λ z eq → o<¬≡ (sym eq) (proj1 (proj2 next-limit) _ (ordtrans <-osuc (subst (λ k → k o< next (osuc x)) eq {!!} )))))
+           (λ z eq → o<¬≡ (sym eq) ((proj1 (proj2 next-limit)) _ (osuc< (sym eq)))))
 
         record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
           field