# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1655140215 -32400
# Node ID d041941a8866c1ed6a90226b7f98daf9a0604770
# Parent  7a6d3f3493954aa0ba3c3c2bfd2bb46d21bc43d4
total done

diff -r 7a6d3f349395 -r d041941a8866 src/zorn.agda
--- a/src/zorn.agda	Tue Jun 14 01:50:31 2022 +0900
+++ b/src/zorn.agda	Tue Jun 14 02:10:15 2022 +0900
@@ -604,9 +604,12 @@
                      um02 i (fsuc j fc) = f-next zb ( um02 j fc )
          u-total : IsTotalOrderSet Uz
          u-total {x} {y} ux uy  with trio< (UZFChain.u ux) (UZFChain.u uy)
-         ... | tri< a ¬b ¬c = ZChain.f-total (uzc uy) (u-mono (UZFChain.u ux) (UZFChain.u uy) {!!} {!!} (uzc ux) (uzc uy) (UZFChain.chain∋z ux)) (UZFChain.chain∋z uy)
-         ... | tri≈ ¬a b ¬c = tri≈ {!!} {!!} {!!}
-         ... | tri> ¬a ¬b c = ZChain.f-total (uzc ux) (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux) {!!} {!!} (uzc uy) (uzc ux) (UZFChain.chain∋z uy)) 
+         ... | tri< a ¬b ¬c = ZChain.f-total (uzc uy) (u-mono (UZFChain.u ux) (UZFChain.u uy)
+            (UZFChain.u<x uy) (ordtrans a <-osuc ) (uzc ux) (uzc uy) (UZFChain.chain∋z ux)) (UZFChain.chain∋z uy)
+         ... | tri≈ ¬a b ¬c = ZChain.f-total (uzc ux) (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
+            (UZFChain.u<x ux) (subst (λ k → k o< osuc (UZFChain.u ux)) b <-osuc) (uzc uy) (uzc ux) (UZFChain.chain∋z uy))
+         ... | tri> ¬a ¬b c = ZChain.f-total (uzc ux) (UZFChain.chain∋z ux) (u-mono (UZFChain.u uy) (UZFChain.u ux)
+            (UZFChain.u<x ux) (ordtrans c <-osuc) (uzc uy) (uzc ux) (UZFChain.chain∋z uy)) 
          
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM