# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1687145603 -32400
# Node ID 4eac5585b6b1fa8b12b9060c5209dc42ad41d235
# Parent  29f686c654bf033fc55f532edb5765999b315532
...

diff -r 29f686c654bf -r 4eac5585b6b1 src/bijection.agda
--- a/src/bijection.agda	Mon Jun 19 11:22:29 2023 +0900
+++ b/src/bijection.agda	Mon Jun 19 12:33:23 2023 +0900
@@ -960,18 +960,25 @@
        lem12 with <-cmp n (fun→  an (Is.a isa)) | c1+1 n i isa
        ... | tri< a ¬b ¬c | eq = ≤-trans (subst (λ k → k ≤ count-A i) eq (c1<ca n i)) a≤sa
        ... | tri≈ ¬a b ¬c | eq = begin
-            c1 n (suc i) ≡⟨ sym eq ⟩
-            suc ( c1 n i) ≤⟨ s≤s (c1<ca n i) ⟩
-            suc (count-A i) ∎ where open ≤-Reasoning
+             c1 n (suc i) ≡⟨ sym eq ⟩
+             suc ( c1 n i) ≤⟨ s≤s (c1<ca n i) ⟩
+             suc (count-A i) ∎ where open ≤-Reasoning
        ... | tri> ¬a ¬b c₁ | eq = begin
-            c1 n (suc i) ≡⟨ sym eq ⟩
-            suc ( c1 n i) ≤⟨ s≤s (c1<ca n i) ⟩
-            suc (count-A i) ∎ where open ≤-Reasoning
+             c1 n (suc i) ≡⟨ sym eq ⟩
+             suc ( c1 n i) ≤⟨ s≤s (c1<ca n i) ⟩
+             suc (count-A i) ∎ where open ≤-Reasoning
        ca01 : c1 (suc n) (suc i) ≤ suc (count-A i)
        ca01 with <-cmp (fun→ cn (g (f (fun← an (suc n))))) (suc i)
-       ... | tri< a ¬b ¬c = lem13 where  -- count-A contains (suc i), so keep ≤-relation
-             lem13 : suc (c1 n (suc i)) ≤ suc (count-A i) 
-             lem13 = ?
+       ... | tri< a ¬b ¬c = lem13 n ≤-refl where  -- count-A contains (suc i), so keep ≤-relation
+             lem13 : (j : ℕ) → j ≤ n → suc (c1 j (suc i)) ≤ suc (count-A i)
+             lem13 0 j≤n with <-cmp (fun→ cn (g (f (fun← an 0)))) (suc i)
+             ... | tri< a ¬b ¬c = ?
+             ... | tri≈ ¬a b ¬c = ?
+             ... | tri> ¬a ¬b c₁ = ?
+             lem13 (suc j) j≤n with <-cmp (fun→ cn (g (f (fun← an (suc j))))) (suc i)
+             ... | tri< a ¬b ¬c = ?
+             ... | tri≈ ¬a b ¬c = ?
+             ... | tri> ¬a ¬b c₁ = ?
        ... | tri≈ ¬a b ¬c = lem13 where  -- count-A contains (suc i) here
              lem15 : c1 n i ≡ c1 n (suc i) 
              lem15 with <-cmp n (fun→ an (Is.a isa)) | c1+1 n i isa 
@@ -979,12 +986,25 @@
              ... | tri≈ ¬a bi ¬c | eq = ⊥-elim ( nat-≡< (sym ( inject-cgf ( trans b lem16 ))) a<sa ) where
                   lem16 : suc i ≡  fun→ cn (g (f (fun← an n )))
                   lem16 = begin 
-                    suc i ≡⟨ sym ( fiso→ cn _) ⟩
-                    fun→ cn (fun← cn (suc i))  ≡⟨ cong (fun→ cn) (sym (Is.fa=c isa)) ⟩
-                    fun→ cn (g (f (Is.a isa)))  ≡⟨ cong (λ k → fun→ cn (g (f k)) ) (sym (fiso← an _)) ⟩
-                    fun→ cn (g (f (fun← an (fun→ an (Is.a isa)))))  ≡⟨  cong (λ k → fun→ cn (g (f (fun← an k))))  (sym bi) ⟩
-                    fun→ cn (g (f (fun← an n ))) ∎ where open ≡-Reasoning
-             ... | tri> ¬a ¬b c₁ | eq = ?
+                       suc i ≡⟨ sym ( fiso→ cn _) ⟩
+                       fun→ cn (fun← cn (suc i))  ≡⟨ cong (fun→ cn) (sym (Is.fa=c isa)) ⟩
+                       fun→ cn (g (f (Is.a isa)))  ≡⟨ cong (λ k → fun→ cn (g (f k)) ) (sym (fiso← an _)) ⟩
+                       fun→ cn (g (f (fun← an (fun→ an (Is.a isa)))))  ≡⟨  cong (λ k → fun→ cn (g (f (fun← an k))))  (sym bi) ⟩
+                       fun→ cn (g (f (fun← an n ))) ∎ where open ≡-Reasoning
+             ... | tri> ¬a ¬b c₁ | eq = ⊥-elim ( nat-≡< refl lem17 ) where
+                  lem18 : fun→ cn (g (f (fun← an (suc n)))) ≡ fun→ cn (g (f (fun← an (fun→ an (Is.a isa)))))
+                  lem18 = begin
+                       fun→ cn (g (f (fun← an (suc n)))) ≡⟨ b ⟩
+                       suc i ≡⟨ sym ( fiso→ cn _) ⟩
+                       fun→ cn (fun← cn (suc i)) ≡⟨ sym (cong (fun→ cn) (Is.fa=c isa)) ⟩
+                       fun→ cn (g (f (Is.a isa))) ≡⟨ cong (λ k → fun→ cn (g (f k))) (sym (fiso← an _)) ⟩
+                       fun→ cn (g (f (fun← an (fun→ an (Is.a isa))))) ∎ where open ≡-Reasoning
+                  lem17 : suc n ≤ n
+                  lem17 = begin
+                       suc n <⟨ s≤s a<sa ⟩
+                       suc (suc n) ≡⟨ cong (λ k → suc k) (inject-cgf lem18 ) ⟩
+                       suc (fun→ an (Is.a isa)) ≤⟨ c₁ ⟩
+                       n ∎ where open ≤-Reasoning
              lem13 : suc (c1 n (suc i)) ≤ suc (count-A i) 
              lem13 = s≤s ( subst (λ k → k ≤ count-A i) lem15 ( c1<ca n i) )
        ... | tri> ¬a ¬b c₁ = lem12 -- count-A is one degree larger now