--- a/Ordinals.agda	Wed Jul 29 00:25:07 2020 +0900
+++ b/Ordinals.agda	Wed Jul 29 12:42:05 2020 +0900
@@ -265,6 +265,38 @@
         omax<next : {x y : Ordinal} → x o< y → omax x y o< next y
         omax<next {x} {y} x<y = subst (λ k → k o< next y ) (omax< _ _ x<y ) (osuc<nx x<nx)
 
+        x<ny→≡next : {x y : Ordinal} → x o< y → y o< next x → next x ≡ next y
+        x<ny→≡next {x} {y} x<y y<nx with trio< (next x) (next y)    
+        x<ny→≡next {x} {y} x<y y<nx | tri< a ¬b ¬c =          -- x < y < next x <  next y ∧ next x = osuc z
+             ⊥-elim ( ¬nx<nx y<nx a (λ z eq →  o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc )))) 
+        x<ny→≡next {x} {y} x<y y<nx | tri≈ ¬a b ¬c = b
+        x<ny→≡next {x} {y} x<y y<nx | tri> ¬a ¬b c =          -- x < y < next y < next x
+             ⊥-elim ( ¬nx<nx (ordtrans x<y x<nx) c (λ z eq →  o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc )))) 
+
+        ≤next : {x y : Ordinal} → x o< y → next x o≤ next y
+        ≤next {x} {y} x<y with trio< (next x) y
+        ≤next {x} {y} x<y | tri< a ¬b ¬c = ordtrans a (ordtrans x<nx <-osuc )
+        ≤next {x} {y} x<y | tri≈ ¬a refl ¬c = (ordtrans x<nx <-osuc )
+        ≤next {x} {y} x<y | tri> ¬a ¬b c = o≤-refl (x<ny→≡next x<y c)
+
+        x<ny→≤next : {x y : Ordinal} → x o< next y → next x o≤ next y
+        x<ny→≤next {x} {y} x<ny with trio< x y
+        x<ny→≤next {x} {y} x<ny | tri< a ¬b ¬c =  ≤next a
+        x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c =  o≤-refl refl
+        x<ny→≤next {x} {y} x<ny | tri> ¬a ¬b c = o≤-refl (sym ( x<ny→≡next c x<ny ))
+
+        omax<nomax : {x y : Ordinal} → omax x y o< next (omax x y )
+        omax<nomax {x} {y} with trio< x y
+        omax<nomax {x} {y} | tri< a ¬b ¬c    = subst (λ k → osuc y o< k ) nexto≡ (osuc<nx x<nx )
+        omax<nomax {x} {y} | tri≈ ¬a refl ¬c = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx )
+        omax<nomax {x} {y} | tri> ¬a ¬b c    = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx )
+
+        omax<nx : {x y z : Ordinal} → x o< next z → y o< next z → omax x y o< next z
+        omax<nx {x} {y} {z} x<nz y<nz with trio< x y
+        omax<nx {x} {y} {z} x<nz y<nz | tri< a ¬b ¬c = osuc<nx y<nz
+        omax<nx {x} {y} {z} x<nz y<nz | tri≈ ¬a refl ¬c = osuc<nx y<nz
+        omax<nx {x} {y} {z} x<nz y<nz | tri> ¬a ¬b c = osuc<nx x<nz
+
         record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
           field
             os→ : (x : Ordinal) → x o< maxordinal → Ordinal