--- a/ordinal.agda	Thu Jun 06 09:36:41 2019 +0900
+++ b/ordinal.agda	Sat Jun 08 13:18:10 2019 +0900
@@ -109,6 +109,18 @@
 ¬a≤a : {la : Nat} → Suc la ≤ la → ⊥
 ¬a≤a  (s≤s lt) = ¬a≤a  lt
 
+=→¬< : {x : Nat  } → ¬ ( x < x )
+=→¬< {Zero} ()
+=→¬< {Suc x} (s≤s lt) = =→¬< lt
+
+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
+
+¬x<0 : {n : Level} →  { x  : Ordinal {suc n} } → ¬ ( x o< o∅ {suc n} )
+¬x<0 {n} {x} (case1 ())
+¬x<0 {n} {x} (case2 ())
+
 o<> : {n : Level} →  {x y : Ordinal {n}  }  →  y o< x → x o< y → ⊥
 o<> {n} {x} {y} (case1 x₁) (case1 x₂) = nat-<>  x₁ x₂
 o<> {n} {x} {y} (case1 x₁) (case2 x₂) = nat-≡< (sym (d<→lv x₂)) x₁