--- a/ordinal.agda	Mon Jul 08 18:26:33 2019 +0900
+++ b/ordinal.agda	Mon Jul 08 19:35:23 2019 +0900
@@ -118,6 +118,14 @@
 =→¬< {Zero} ()
 =→¬< {Suc x} (s≤s lt) = =→¬< lt
 
+case12-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord x d< ord y → ⊥
+case12-⊥ {x} {y} lt1 lt2 with d<→lv lt2
+... | refl = nat-≡< refl lt1
+
+case21-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord y d< ord x → ⊥
+case21-⊥ {x} {y} lt1 lt2 with d<→lv lt2
+... | refl = nat-≡< refl lt1
+
 o<¬≡ : {n : Level } { ox oy : Ordinal {n}} → ox ≡ oy  → ox o< oy  → ⊥
 o<¬≡ {_} {ox} {ox} refl (case1 lt) =  =→¬< lt
 o<¬≡ {_} {ox} {ox} refl (case2 (s< lt)) = trio<≡ refl lt