# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1687055820 -32400
# Node ID 575777026a7269350d21d8beb9ceef7c0faefe6e
# Parent  f5048a51d19ffb7728ea5d1a628edb8fa56822f1
...

diff -r f5048a51d19f -r 575777026a72 src/bijection.agda
--- a/src/bijection.agda	Sun Jun 18 06:00:57 2023 +0900
+++ b/src/bijection.agda	Sun Jun 18 11:37:00 2023 +0900
@@ -899,12 +899,31 @@
     ... | yes isa | tri≈ ¬a b ¬c = ≤-refl
     ... | yes isa | tri> ¬a ¬b c₁ = a≤sa
     c1<count-A (suc n) zero with is-A (fun← cn zero) |  <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero
-    ... | no nisa | s = ?
-    ... | yes isa | tri≈ ¬a b ¬c = ? where
-         -- only one a in c1 n loop
-         lem00 : c1 n zero ≤ count-A zero
-         lem00 = c1<count-A n zero
-    ... | yes isa | tri> ¬a ¬b c₁ = ?
+    ... | no nisa | tri≈ ¬a b ¬c = ⊥-elim ( nisa record { a = fun← an (suc n) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) b ) } )
+    ... | no nisa | tri> ¬a ¬b c₁ = lem01 n ≤-refl where
+         lem01 : (i : ℕ) → i ≤ n → c1 i 0 ≤ 0
+         lem01 0 i≤n with <-cmp (fun→ cn (g (f (fun← an 0)))) zero
+         ... | tri> ¬a ¬b c₁ = ≤-refl
+         ... | tri≈ ¬a bi ¬c = ⊥-elim ( nisa record { a = fun← an 0 ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) bi) } )
+         lem01 (suc i) i≤n with <-cmp (fun→ cn (g (f (fun← an (suc i))))) zero
+         ... | tri≈ ¬a bi ¬c = ⊥-elim ( nisa record { a = fun← an (suc i) ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) bi) } )
+         lem01 (suc i) (s≤s i≤n) | tri> ¬a ¬b c₁ = lem01 i (≤-trans i≤n a≤sa)
+    ... | yes isa | tri≈ ¬a b ¬c = lem01 n ≤-refl where
+         lem01 : (i : ℕ) → i ≤ n → suc (c1 i 0) ≤ 1 
+         lem01 0 i≤n with <-cmp (fun→ cn (g (f (fun← an 0)))) zero
+         ... | tri> ¬a ¬b c₁ = ≤-refl 
+         ... | tri≈ ¬a bi ¬c = ⊥-elim (nat-≡< (inject-cgf (trans bi (sym b)) ) (<-transʳ i≤n a<sa  ))
+         lem01 (suc i) i≤n with <-cmp (fun→ cn (g (f (fun← an (suc i))))) zero
+         ... | tri≈ ¬a bi ¬c = ⊥-elim (nat-≡< (inject-cgf (trans bi (sym b)) ) (<-transʳ i≤n a<sa  ))
+         lem01 (suc i) (s≤s i≤n) | tri> ¬a ¬b c₁ = lem01 i (≤-trans i≤n a≤sa)
+    ... | yes isa | tri> ¬a ¬b c₁ = lem01 n ≤-refl where
+         lem01 : (i : ℕ) → i ≤ n → c1 i 0 ≤ 1 
+         lem01 0 i≤n with <-cmp (fun→ cn (g (f (fun← an 0)))) zero
+         ... | tri> ¬a ¬b c₁ = a≤sa
+         ... | tri≈ ¬a bi ¬c = ≤-refl
+         lem01 (suc i) i≤n with <-cmp (fun→ cn (g (f (fun← an (suc i))))) zero
+         ... | tri≈ ¬a bi ¬c = ?
+         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 zero) |  <-cmp (fun→ cn (g (f (fun← an (suc n))))) zero
     ... | no nisa | t = ?