--- a/src/bijection.agda	Tue Jun 20 12:14:12 2023 +0900
+++ b/src/bijection.agda	Tue Jun 20 12:52:47 2023 +0900
@@ -578,14 +578,13 @@
     c< zero = ≤-refl
     c< (suc i) = x≤max _ _
 
-    c-mono : {i n : ℕ} → i ≤ n → c i ≤ c n
-    c-mono {zero} {zero} z≤n = ≤-refl
-    c-mono {zero} {suc n} z≤n = ≤-trans (c-mono {zero} {n} z≤n) (y≤max _ _ )
-    c-mono {suc i} {suc n} (s≤s i≤n) with <-cmp (fun→ cn (g (f (fun← an (suc i))))) (c i)
-    ... | tri< a ¬b ¬c = subst (λ k → k ≤ _ ) (sym (x≤y→max=y _ _ (≤-trans a≤sa a ))) (≤-trans ( c-mono {i} {n} i≤n ) ( y≤max _ _ ))
-    ... | tri≈ ¬a b ¬c = subst (λ k → k ≤ _ ) (sym (x≤y→max=y _ _ (subst (λ k → k ≤ c i) (sym b) ≤-refl ))) 
-         (≤-trans ( c-mono {i} {n} i≤n ) ( y≤max _ _ ))
-    ... | tri> ¬a ¬b c₁ = ≤-trans (≤-trans ? ( c< (suc i) )) ?
+    c-mono1 : (i : ℕ) → c i ≤ c (suc i)
+    c-mono1 i = y≤max _ _
+    c-mono : (i j : ℕ ) → i ≤ j → c i ≤ c j
+    c-mono i j i≤j with ≤-∨ i≤j
+    ... | case1 refl = ≤-refl
+    c-mono zero (suc j) z≤n | case2 lt = ≤-trans (c-mono zero j z≤n ) (c-mono1 j) 
+    c-mono (suc i) (suc j) (s≤s i≤j) | case2 (s≤s lt) = ≤-trans (c-mono (suc i) j lt ) (c-mono1 j)
 
     inject-cgf : {i j : ℕ} → fun→ cn (g (f (fun← an i))) ≡ fun→ cn (g (f (fun← an j))) → i ≡ j
     inject-cgf {i} {j} eq = bi-inject← an (InjectiveF.inject fi (InjectiveF.inject gi ( bi-inject→ cn eq )))