--- a/src/bijection.agda	Sun Jun 18 16:18:02 2023 +0900
+++ b/src/bijection.agda	Sun Jun 18 18:16:03 2023 +0900
@@ -933,12 +933,26 @@
          lem01 (suc i) (s≤s i≤n) | tri> ¬a ¬b c₁ = lem01 i (≤-trans i≤n a≤sa)
     c1<count-A zero (suc i) = ?
     c1<count-A (suc n) (suc i) with is-A (fun← cn (suc i)) |  <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i)
-    ... | no nisa | tri< a ¬b ¬c = subst (λ k → k ≤ count-A i) (sym (lem11 n ≤-refl)) lem10 where
+    ... | no nisa | tri< a ¬b ¬c = ? where -- subst (λ k → k ≤ count-A i) (sym (lem11 n ≤-refl)) lem10 where
+          lem12 : suc (c1 n (suc i)) ≤ count-A i
+          lem12 = ?
+          lem13 : c1 n i ≡ c1 n (suc i) 
+          lem13 = c1+0 {n} {i} nisa
           lem10 : c1 n i ≤ count-A i
           lem10 = c1<count-A n i
+          lem14 : suc (c1 n i) ≤ count-A i   -- becase count-A i contains (ani (suc n))
+          lem14 = ?
           lem11 : (j : ℕ ) → j ≤ n → suc (c1 j (suc i)) ≡ c1 j i 
           lem11 zero j≤n with <-cmp (fun→ cn (g (f (fun← an zero)))) i | <-cmp (fun→ cn (g (f (fun← an zero)))) (suc i) 
-          ... | t | s = ?
+          ... | tri< a₂ ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = ?
+          ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim ( nisa record { a = fun← an 0  ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) b) })
+          ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = refl
+          ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ?
+          ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = ?
+          ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ?
+          ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c = ?
+          ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ?
+          ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = ?
           lem11 (suc j) j≤n with <-cmp (fun→ cn (g (f (fun← an (suc j))))) i | <-cmp (fun→ cn (g (f (fun← an (suc j)))))  (suc i)
           ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = cong suc (lem11 j (≤-trans a≤sa j≤n ) )
           ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = cong suc (lem11 j  (≤-trans a≤sa j≤n ))
@@ -946,9 +960,8 @@
           ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = cong suc (lem11 j  (≤-trans a≤sa j≤n ))
           ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = cong suc (lem11 j  (≤-trans a≤sa j≤n ))
           ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≡< (sym b) (<-trans a<sa c₁) )
-          ... | tri> ¬a ¬b c₁ | tri< a₁ ¬b₁ ¬c = ? where
-               -- suc (fun→ cn (g (i (fun← an (suc j))))) ≡ suc i
-          ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ?
+          ... | tri> ¬a ¬b c₁ | tri< (s≤s a₁) ¬b₁ ¬c = ⊥-elim (nat-≤> a₁ c₁ )
+          ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ⊥-elim ( nisa record { a = fun← an (suc j) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) b) })  
           ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = lem11 j  (≤-trans a≤sa j≤n )
     ... | no nisa | tri≈ ¬a b ¬c = ?
     ... | no nisa | tri> ¬a ¬b c₁ = ?