# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1594692729 -32400
# Node ID e277699923993f1bd91b34cb7c727725c96bc5f2
# Parent  08d94fec239c42ae4916d86a3388606b72285717
next-is-limit

diff -r 08d94fec239c -r e27769992399 Ordinals.agda
--- a/Ordinals.agda	Tue Jul 14 07:59:17 2020 +0900
+++ b/Ordinals.agda	Tue Jul 14 11:12:09 2020 +0900
@@ -251,6 +251,11 @@
         nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx<nx (ordtrans <-osuc x<nx) c
            (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
 
+        next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y)
+        next-is-limit {x} {y} eq = o<¬≡ (sym eq) (osuc<nx y<nx) where
+            y<nx : y o< next x
+            y<nx = osuc< (sym eq)
+
         record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
           field
             os→ : (x : Ordinal) → x o< maxordinal → Ordinal