--- a/src/OrdUtil.agda	Fri Jul 15 12:35:59 2022 +0900
+++ b/src/OrdUtil.agda	Fri Jul 15 14:14:53 2022 +0900
@@ -47,6 +47,12 @@
 ... | case1 eq = o<¬≡ (sym eq) (proj1 P) 
 ... | case2 lt = o<> lt (proj1 P) 
 
+b<x→0<x : { p b : Ordinal } → p o< b →  o∅  o< b
+b<x→0<x {p} {b} p<b with trio< o∅ b
+... | tri< a ¬b ¬c = a
+... | tri≈ ¬a 0=b ¬c = ⊥-elim ( ¬x<0 ( subst (λ k → p o< k) (sym 0=b) p<b ) )
+... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
+
 osucc :  {ox oy : Ordinal } → oy o< ox  → osuc oy o< osuc ox  
 osucc {ox} {oy} oy<ox with trio< (osuc oy) ox
 osucc {ox} {oy} oy<ox | tri< a ¬b ¬c = ordtrans a <-osuc