# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1686368233 -32400
# Node ID 8cd1956796868995ff3bc1defbb434560ba80e21
# Parent  b8489dcae23654967299492976abc07f035bff2a
...

diff -r b8489dcae236 -r 8cd195679686 src/bijection.agda
--- a/src/bijection.agda	Sat Jun 10 11:47:43 2023 +0900
+++ b/src/bijection.agda	Sat Jun 10 12:37:13 2023 +0900
@@ -627,14 +627,18 @@
                 --
                 lem31 :  suc j < count-A (fun→ cn (g (f (fun← an (suc j))))) 
                 lem31 with <∨≤  (suc j) (fun→ cn (g (f (fun← an (suc j)))))
-                ... | case1 lt = lem12 _ refl  where
-                     lem12 : (i : ℕ) → i ≡ fun→ cn (g (f (fun← an (suc j)))) → suc j < count-A (fun→ cn (g (f (fun← an (suc j))))) 
-                     lem12 zero i=z with is-A (fun← cn  zero) | inspect ( count-A ) zero
-                     ... | yes isa | record { eq = eq1 } = ?
-                     ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = trans (sym (fiso←  cn _)) (sym (cong (fun← cn) ? ))  } ) 
-                     lem12 (suc i) i=z with is-A (fun← cn  (suc i)) | inspect ( count-A ) (suc i)
-                     ... | yes isa | record { eq = eq1 } = ?
-                     ... | no nisa | record { eq = eq1 } = ⊥-elim ( nisa record { a = fun← an zero ; fa=c = trans (sym (fiso←  cn _)) (sym (cong (fun← cn) ?))  } ) 
+                ... | case1 lt = lem12 _ lt ≤-refl  where
+                     lem13 : suc j < fun→ cn (g (f (fun← an (suc j))))
+                     lem13 = lt
+                     -- suc j is current count of A
+                     -- it increase at fun→ cn (g (f (fun← an (suc j))))
+                     -- otherwise ≤
+                     lem12 : (i : ℕ) → suc j < i  → i ≤ fun→ cn (g (f (fun← an (suc j)))) → suc j < count-A i
+                     lem12 (suc i) (s≤s sj<i) i≤fj with ≤-∨ sj<i
+                     ... | case1 eq = ?
+                     ... | case2 lt = ? where
+                         lem14 : suc j < count-A i
+                         lem14 = lem12 i lt (≤-trans refl-≤s i≤fj)
                 ... | case2 le = ? where
                      -- count-A<i : (i : ℕ) → count-A i ≤ suc i
                      lem33 : (i : ℕ) → i ≡ fun→ cn (g (f (fun← an (suc j)))) →  ¬ (i ≤ maxAC.ac (lem10 j))