# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1686400059 -32400
# Node ID c7623ec8f0d33b68d1eafeed51fe68a389b2282d
# Parent  579f1bf9122cb19110e6f253a9b612fe8e490312
...

diff -r 579f1bf9122c -r c7623ec8f0d3 src/bijection.agda
--- a/src/bijection.agda	Sat Jun 10 20:50:18 2023 +0900
+++ b/src/bijection.agda	Sat Jun 10 21:27:39 2023 +0900
@@ -604,14 +604,12 @@
                 lem12 (suc i) i=z with is-A (fun← cn  (suc i)) | inspect ( count-A ) (suc i)
                 ... | yes isa | record { eq = eq1 } = record { ac = suc i ; n<ca = subst (λ k → 0 < k) (sym eq1) 0<s ; all-a = ? }
                 ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an zero ; fa=c = trans (sym (fiso←  cn _)) (sym (cong (fun← cn) i=z))  } ) 
-            lem10 (suc j) = ? where
+            lem10 (suc j) = record { ac = nac ; n<ca = ? ; all-a = ? } where
                 -- 
                 --   maxAC n contains at least n elements of A
                 --
-                lem31 : maxAC (suc j)
-                lem31 with <∨≤  (maxAC.ac (lem10 j))  (fun→ cn (g (f (fun← an (suc j)))))
-                ... | case1 lt = record { ac = (fun→ cn (g (f (fun← an (suc j))))) ; n<ca = ? ; all-a = ? }
-                ... | case2 le = record { ac = (maxAC.ac (lem10 j)) ; n<ca = ? ; all-a = ? }
+                nac : ℕ
+                nac = max (fun→ cn (g (f (fun← an (suc j))))) (maxAC.ac (lem10 j))
 
     lem01 : (n i : ℕ) → n < count-B i → B
     lem01 zero zero lt with is-B (fun← cn zero)
@@ -620,12 +618,13 @@
     lem01 zero (suc i) lt with is-B (fun← cn (suc i))
     ... | yes isB = Is.a isB
     ... | no nisB = lem01 zero i lt 
-    lem01 (suc n) zero lt with is-B (fun← cn zero)
-    ... | yes isB = Is.a isB
-    ... | no nisB = ⊥-elim (nat-≤>  lt 0<s )
+    lem01 (suc n) zero lt = ? -- cannot happen
     lem01 (suc n) (suc i) lt with is-B (fun← cn (suc i))
-    ... | yes isB = Is.a isB
     ... | no nisB = lem01 (suc n) i lt 
+    ... | yes isB with <-cmp n i
+    ... | tri< a ¬b ¬c = lem01 n i ?
+    ... | tri≈ ¬a b ¬c = Is.a isB
+    ... | tri> ¬a ¬b c = ? -- cannot happen
 
     ntob : (n : ℕ) → B
     ntob n = lem01 n (maxAC.ac (lem02 n)) (≤-trans (maxAC.n<ca (lem02 n)) (ca≤cb0 (maxAC.ac (lem02 n))) )