--- a/src/bijection.agda	Thu Jun 22 07:38:29 2023 +0900
+++ b/src/bijection.agda	Thu Jun 22 09:20:17 2023 +0900
@@ -678,8 +678,7 @@
     any-cl i cl = (j : ℕ) → j ≤ i → Any (_≡_ (g (f (fun← an j)))) cl
 
     n<ca-list : (n : ℕ) → n < ca-list (clist (c n))
-    n<ca-list zero = subst ( λ k → zero < k ) (a-list-ca zero (clist (c zero)) (clist-any zero zero ≤-refl)) ( <-transˡ a<sa (s≤s z≤n )) 
-    n<ca-list (suc n) = lem06 where
+    n<ca-list n = lem30 n (clist (c n)) ≤-refl (λ j le  → clist-any n j le ) where
          --
          --  we have ANY i on i ≤ n, so we can remove n element from clist (c n)
          --  induction on n is no good, because (ani (suc n)) may happen in clist (c n)
@@ -704,25 +703,17 @@
               → suc (ca-list (del i cl a)) ≡ ca-list cl
          del-ca i cl a = a-list-ca i cl (a i ≤-refl) 
 
-         lem06 : suc n < ca-list (clist (c (suc n)))
-         lem06 = lem31 where
-            lem30 : (i : ℕ) → (cl : List C) → (i≤n : i ≤ suc n) → (a : any-cl (suc i) cl) → suc i < ca-list cl
-            lem30 0 cl i≤n a = begin
-                2 ≤⟨ s≤s (s≤s z≤n) ⟩ 
-                suc (suc (ca-list (del 0 (del 1 cl a) (del-any 0 cl a)) )) ≡⟨ cong suc ( del-ca 0 (del 1 cl a) (del-any 0 cl a)) ⟩ 
-                suc (ca-list (del 1 cl a) )  ≡⟨ del-ca 1 cl a ⟩ 
-                ca-list cl ∎ where
-                   open ≤-Reasoning
-            lem30 (suc i) cl i≤n a = begin
-               suc (suc (suc i))   ≤⟨ s≤s (lem30 i _ (≤-trans a≤sa i≤n) (del-any (suc i) cl a) ) ⟩ 
-               suc (ca-list (del (suc (suc i)) cl a))  ≡⟨ del-ca (suc (suc i)) cl a ⟩ 
-               ca-list cl ∎ where
-                   open ≤-Reasoning
-            lem31 : suc n < ca-list (clist (c (suc n)))
-            lem31 = lem30 n (clist (c (suc n))) a≤sa (λ j le  → clist-any (suc n) j le )
-
-    n<ca0 : {n : ℕ} → n < count-A (c n)
-    n<ca0 = ? 
+         lem30 : (i : ℕ) → (cl : List C) → (i≤n : i ≤ n) → (a : any-cl i cl) → i < ca-list cl
+         lem30 0 cl i≤n a = begin
+             1 ≤⟨ s≤s z≤n ⟩ 
+             suc (ca-list (del 0 cl a) )  ≡⟨ del-ca 0 cl a ⟩
+             ca-list cl ∎ where
+                open ≤-Reasoning
+         lem30 (suc i) cl i≤n a = begin
+            suc (suc i)   ≤⟨ s≤s (lem30 i _ (≤-trans a≤sa i≤n) (del-any i cl a) ) ⟩ 
+            suc (ca-list (del (suc i) cl a))  ≡⟨ del-ca (suc i) cl a ⟩ 
+            ca-list cl ∎ where
+                open ≤-Reasoning
 
     record maxAC (n : ℕ) : Set where
        field
@@ -730,24 +721,32 @@
            n<ca : n < count-A ac
 
     lem02 : (n : ℕ) → maxAC n
-    lem02 n = record { ac = c n ; n<ca = ? }
+    lem02 n = record { ac = c n ; n<ca = subst (λ k → n < k) (ca-list=count-A (c n)) (n<ca-list n ) }
 
     record CountB (n : ℕ) : Set where
        field
           b : B
           cb : ℕ
           b=cn : fun← cn cb ≡ g b
-          cb=n : count-B cb ≡ n
+          cb=n : count-B cb ≡ suc n
 
     lem01 : (n i : ℕ) → suc n ≤ count-B i → CountB n
-    lem01 zero zero lt = record { b = ? ; cb = zero ; b=cn = ? ; cb=n = ? }
-    lem01 zero (suc i) lt = record { b = ? ; cb = zero ; b=cn = ? ; cb=n = ? }
+    lem01 zero zero le with is-B (fun← cn 0) | inspect count-B zero
+    ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = eq1 } 
+    ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≤> le a<sa)
+    lem01 zero (suc i) le  with ≤-∨ le
+    ... | case1 eq with is-B (fun← cn (suc i)) | inspect count-B (suc i)
+    ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 (sym eq) } 
+    ... | no nisb | record { eq = eq1 } = lem01 zero i le
+    lem01 zero (suc i) le  | case2 lt with is-B (fun← cn (suc i)) | inspect count-B (suc i)
+    ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 ? }
+    ... | no nisb | record { eq = eq1 } = lem01 zero i le
     lem01 (suc n) zero ()
     lem01 (suc n) (suc i) n≤i with is-B (fun← cn (suc i))
     ... | no nisB = lem01 (suc n) i n≤i
     ... | yes isB with <-cmp (count-B (suc i)) (suc n)
     ... | tri< a ¬b ¬c = lem01 (suc n) i ?
-    ... | tri≈ ¬a eq ¬c = record { b = Is.a isB ; cb = suc i ; b=cn = sym (Is.fa=c isB) ; cb=n = eq }
+    ... | tri≈ ¬a eq ¬c = record { b = Is.a isB ; cb = suc i ; b=cn = sym (Is.fa=c isB) ; cb=n = ? }
     ... | tri> ¬a ¬b c = lem01 (suc n) i ?