--- a/src/bijection.agda	Sat Jun 17 10:05:20 2023 +0900
+++ b/src/bijection.agda	Sat Jun 17 11:05:09 2023 +0900
@@ -715,7 +715,18 @@
     c1+1 : (n i : ℕ) → (isa : Is A C (λ x → g (f x)) (fun← cn i)) 
         →  c1+1P n i isa 
     c1+1 0 i isa with <-cmp 0 (fun→  an (Is.a isa))
-    ... | tri< n<an ¬b ¬c = ?
+    ... | tri< n<an ¬b ¬c = c123 where
+         c123 : c1 zero i ≡ c1 zero (suc i)
+         c123 with <-cmp (ani 0) i | <-cmp (ani 0) (suc i)
+         ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = refl
+         ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = refl
+         ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c₁ = ⊥-elim ( nat-≤> refl-≤s (<-trans c₁ a) )
+         ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = refl
+         ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl
+         ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c₁ = ⊥-elim ( nat-≤> (subst (λ k → k ≤ _) (sym b) a≤sa ) c₁  )
+         ... | tri> ¬a ¬b c₁ | tri< a ¬b₁ ¬c = ⊥-elim ( nat-≤> a (s≤s c₁))
+         ... | tri> ¬a ¬b c₁ | tri≈ ¬a₁ b ¬c = ?     -- ani 0 ≡ suc i, ani ? ≡ i
+         ... | tri> ¬a ¬b c₁ | tri> ¬a₁ ¬b₁ c₂ = refl
     ... | 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

--- a/src/nat.agda	Sat Jun 17 10:05:20 2023 +0900
+++ b/src/nat.agda	Sat Jun 17 11:05:09 2023 +0900
@@ -231,6 +231,8 @@
 refl-≤s {zero} = z≤n
 refl-≤s {suc x} = s≤s (refl-≤s {x})
 
+a≤sa = refl-≤s
+
 refl-≤ : {x : ℕ } → x ≤ x
 refl-≤ {zero} = z≤n
 refl-≤ {suc x} = s≤s (refl-≤ {x})