--- a/ordinal.agda	Wed Jun 05 14:35:32 2019 +0900
+++ b/ordinal.agda	Wed Jun 05 18:24:32 2019 +0900
@@ -242,6 +242,15 @@
 omxxx : {n : Level} ( x : Ordinal {suc n} ) → omax x (omax x x ) ≡ osuc (osuc x)
 omxxx {n} x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc ))
 
+open _∧_
+
+osuc2 : {n : Level} ( x y : Ordinal {suc n} ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
+proj1 (osuc2 {n} x y) (case1 lt) = case1 lt
+proj1 (osuc2 {n} x y) (case2 (s< lt)) = case2 lt
+proj2 (osuc2 {n} x y) (case1 lt) = case1 lt
+proj2 (osuc2 {n} x y) (case2 lt) with d<→lv lt
+... | refl = case2 (s< lt)
+
 -- omax≡ (omax x x ) (osuc x) (omxx x)
 
 OrdTrans : {n : Level} → Transitive {suc n} _o≤_