# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1593888341 -32400
# Node ID feeba7fd499a538493097fb75c1a5eb98c82e603
# Parent  1a54dbe1ea4c261c02dca9fb0cb6303158aa450d
...

diff -r 1a54dbe1ea4c -r feeba7fd499a OD.agda
--- a/OD.agda	Sat Jul 04 22:48:49 2020 +0900
+++ b/OD.agda	Sun Jul 05 03:45:41 2020 +0900
@@ -330,7 +330,9 @@
         lemma3 : {x : HOD} → od→ord (u x) o< osuc (od→ord ( Union (u x , (u x , u x))   ))
         lemma3 {x} = od⊆→o≤ lemma1
         lemma4 : {x : HOD} → od→ord (u x) o< osuc (osuc (od→ord x))
-        lemma4 {x} = ordtrans (<odmax (x , x) {!!}) {!!}
+        lemma4 {x} = ordtrans (<odmax (u x , u x) (case2 refl)) 
+           (subst (λ k → k o< osuc (osuc (od→ord x))) (omax≡ _ _ refl) ( -- odmax (u x , u x) o< osuc (osuc (od→ord x))
+            osucc {!!} )) -- osuc (od→ord (u x)) o<  osuc (osuc (od→ord x))
         lemma : {y : Ordinal} → infinite-d y → y o< next o∅ 
         lemma {y} = TransFinite {λ x → infinite-d x → x o<  next o∅ } ind y where
            ind : (x : Ordinal) → ((z : Ordinal) → z o< x → infinite-d z → z o< (next o∅))  →
diff -r 1a54dbe1ea4c -r feeba7fd499a Ordinals.agda
--- a/Ordinals.agda	Sat Jul 04 22:48:49 2020 +0900
+++ b/Ordinals.agda	Sun Jul 05 03:45:41 2020 +0900
@@ -111,7 +111,7 @@
         proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy 
 
         _o≤_ :  Ordinal → Ordinal → Set  n
-        a o≤ b  = (a ≡ b)  ∨ ( a o< b )
+        a o≤ b  = a o< osuc b -- (a ≡ b)  ∨ ( a o< b )
 
 
         xo<ab :  {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa  → ox o< ob ) → oa o< osuc ob
@@ -183,11 +183,14 @@
 
         open _∧_
 
+        o≤-refl :  { i  j : Ordinal } → i ≡ j → i o≤ j
+        o≤-refl {i} {j} eq = subst (λ k → i o< osuc k ) eq <-osuc
         OrdTrans :  Transitive  _o≤_
-        OrdTrans (case1 refl) (case1 refl) = case1 refl
-        OrdTrans (case1 refl) (case2 lt2) = case2 lt2
-        OrdTrans (case2 lt1) (case1 refl) = case2 lt1
-        OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y)
+        OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c
+        OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc
+        OrdTrans a≤b b≤c | case1 refl | case2 a≤c = ordtrans a≤c <-osuc
+        OrdTrans a≤b b≤c | case2 a≤c | case1 refl = ordtrans a≤c <-osuc
+        OrdTrans a≤b b≤c | case2 a<b | case2 b<c = ordtrans (ordtrans a<b  b<c) <-osuc
 
         OrdPreorder :   Preorder n n n
         OrdPreorder  = record { Carrier = Ordinal
@@ -195,7 +198,7 @@
            ; _∼_   = _o≤_
            ; isPreorder   = record {
                 isEquivalence = record { refl = refl  ; sym = sym ; trans = trans }
-                ; reflexive     = case1 
+                ; reflexive     = o≤-refl
                 ; trans         = OrdTrans 
              }
          }