# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1687072682 -32400
# Node ID bb4cd803538345ef69e97543e8998195bd607c4a
# Parent  4c9ec06aafeb9f36095484f46f8325a4de46cd7b
...

diff -r 4c9ec06aafeb -r bb4cd8035383 src/bijection.agda
--- a/src/bijection.agda	Sun Jun 18 12:16:29 2023 +0900
+++ b/src/bijection.agda	Sun Jun 18 16:18:02 2023 +0900
@@ -933,9 +933,23 @@
          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 = ? where
-          lem10 : c1 n (suc i) ≤ count-A (suc i)
-          lem10 = c1<count-A n (suc i)
+    ... | no nisa | tri< a ¬b ¬c = subst (λ k → k ≤ count-A i) (sym (lem11 n ≤-refl)) lem10 where
+          lem10 : c1 n i ≤ count-A i
+          lem10 = c1<count-A n i
+          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 = ?
+          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 ))
+          ... | tri< a₁ ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⊥-elim ( nat-≡< refl ( <-trans a₁ (<-trans a<sa c₁ )))
+          ... | 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> ¬a₁ ¬b₁ c₂ = lem11 j  (≤-trans a≤sa j≤n )
     ... | no nisa | tri≈ ¬a b ¬c = ?
     ... | no nisa | tri> ¬a ¬b c₁ = ?
     ... | yes isa | tri< a ¬b ¬c = ?