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

diff -r 4eac5585b6b1 -r 88356bb882d4 src/bijection.agda
--- a/src/bijection.agda	Mon Jun 19 12:33:23 2023 +0900
+++ b/src/bijection.agda	Mon Jun 19 12:40:47 2023 +0900
@@ -976,8 +976,12 @@
              ... | 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 = lem16 where
+                  lem16 : suc (suc (c1 j (suc i))) ≤ suc (count-A i)
+                  lem16 = ?
+                  lme14 : suc (c1 j (suc i)) ≤ suc (count-A i)
+                  lme14 = lem13 j ?
+             ... | tri≈ ¬a b ¬c = ? -- cong suc (lem13 j ?)
              ... | tri> ¬a ¬b c₁ = ?
        ... | tri≈ ¬a b ¬c = lem13 where  -- count-A contains (suc i) here
              lem15 : c1 n i ≡ c1 n (suc i)