--- a/src/bijection.agda	Sat Jun 17 09:31:00 2023 +0900
+++ b/src/bijection.agda	Sat Jun 17 10:05:20 2023 +0900
@@ -714,10 +714,28 @@
 
     c1+1 : (n i : ℕ) → (isa : Is A C (λ x → g (f x)) (fun← cn i)) 
         →  c1+1P n i isa 
-    c1+1 n i isa with <-cmp n (fun→  an (Is.a isa))
-    ... | tri< j<an ¬b ¬c = ?
-    ... | tri≈ ¬a j=an ¬c = ?
-    ... | tri> ¬a ¬b an<j = ?
+    c1+1 0 i isa with <-cmp 0 (fun→  an (Is.a isa))
+    ... | tri< n<an ¬b ¬c = ?
+    ... | tri≈ ¬a n=an ¬c = ?
+    c1+1 (suc n) i isa with <-cmp (suc n) (fun→  an (Is.a isa))
+    ... | tri< n<an ¬b ¬c = ? where
+         c110 : c1 n i ≡ c1 n (suc i)
+         c110 with <-cmp n (fun→  an (Is.a isa)) | c1+1 n i isa
+         ... | tri< a ¬b ¬c | s = s
+         ... | tri≈ ¬a b ¬c | s = ⊥-elim ( nat-≡< b (<-trans a<sa n<an ))
+         ... | tri> ¬a ¬b c₁ | s = ⊥-elim ( nat-≤> c₁ (<-trans (<-trans a<sa a<sa) (<-transʳ n<an a<sa ) ))
+    ... | tri≈ ¬a n=an ¬c = ? where
+         c111 : c1 n i ≡ c1 n (suc i)
+         c111 with <-cmp n (fun→  an (Is.a isa)) | c1+1 n i isa
+         ... | tri< a ¬b ¬c | s = s
+         ... | tri≈ ¬a b ¬c | s = ⊥-elim ( nat-≡< b (subst (λ k → n < k ) n=an a<sa ))
+         ... | tri> ¬a ¬b c₁ | s = ⊥-elim ( nat-≡< (sym n=an) (<-trans c₁ a<sa ))
+    ... | tri> ¬a ¬b an<j = ? where
+         c112 : suc (c1 n i) ≡ c1 n (suc i)
+         c112 with <-cmp n (fun→  an (Is.a isa)) | c1+1 n i isa
+         ... | tri< a ¬b ¬c | s = ⊥-elim (nat-≤> an<j (<-transʳ a a<sa) )
+         ... | tri≈ ¬a b ¬c | s = s
+         ... | tri> ¬a ¬b c₁ | s = s
 
     record maxAC (n : ℕ) : Set where
        field