diff Ordinals.agda @ 338:bca043423554

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 12 Jul 2020 12:32:42 +0900
parents 0faa7120e4b5
children feb0fcc430a9
line wrap: on
line diff
--- a/Ordinals.agda	Tue Jul 07 15:32:11 2020 +0900
+++ b/Ordinals.agda	Sun Jul 12 12:32:42 2020 +0900
@@ -106,6 +106,12 @@
         osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case1 eq = ⊥-elim (o<¬≡ (sym eq) oy<ox)
         osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case2 lt = ⊥-elim (o<> lt oy<ox)
 
+        osucprev :  {ox oy : Ordinal } → osuc oy o< osuc ox  → oy o< ox  
+        osucprev {ox} {oy} oy<ox with trio< oy ox
+        osucprev {ox} {oy} oy<ox | tri< a ¬b ¬c = a
+        osucprev {ox} {oy} oy<ox | tri≈ ¬a b ¬c = ⊥-elim (o<¬≡ (cong (λ k → osuc k) b) oy<ox )
+        osucprev {ox} {oy} oy<ox | tri> ¬a ¬b c = ⊥-elim (o<> (osucc c) oy<ox )
+
         open _∧_
 
         osuc2 :  ( x y : Ordinal  ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)