# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1686626884 -32400
# Node ID 87df366f85f367b4b4b5413a9ad7d7aaafc952fd
# Parent  97ea311161ba026a9ca304e822026f59a3eb96ec
...

diff -r 97ea311161ba -r 87df366f85f3 src/bijection.agda
--- a/src/bijection.agda	Tue Jun 13 12:04:49 2023 +0900
+++ b/src/bijection.agda	Tue Jun 13 12:28:04 2023 +0900
@@ -794,12 +794,12 @@
              cl02 = n<ca fl i ?
              cl05 : count-A (c fl 0 ?) ≡  count-A (c (cons (ca<n j fi<fm) fl fr) 0 ? ) 
              cl05 = ?
-             cl06 : count-A (c fl i ?) ≡  count-A (c (cons (ca<n j fi<fm) fl fr) (suc i) ? ) 
+             cl06 : suc (count-A (c fl i ?)) ≤  count-A (c (cons (ca<n j fi<fm) fl fr) (suc i) ? ) 
              cl06 = ?
              cl03 : (suc i) + count-A (c (cons (ca<n j fi<fm) fl fr) 0 ?) ≤ count-A (c (cons (ca<n j fi<fm) fl fr) (suc i) ? )
              cl03 = begin
                  (suc i) + count-A (c (cons (ca<n j fi<fm) fl fr) 0 ?) ≡⟨ ? ⟩
-                 (suc i) + count-A (c fl 0 ?) ≤⟨ ? ⟩
+                 (suc i) + count-A (c fl 0 ?) ≡⟨ ? ⟩
                  suc (i + count-A (c fl 0 ?)) ≤⟨ ? ⟩
                  suc (count-A (c fl i ?)) ≤⟨ ? ⟩
                  count-A (c (cons (ca<n j fi<fm) fl fr) (suc i) ? ) ∎ where